diff options
| author | Théo Zimmermann | 2019-12-22 20:52:01 +0100 |
|---|---|---|
| committer | GitHub | 2019-12-22 20:52:01 +0100 |
| commit | 273586eca1f6372d3b633b7689b9cbb33d4e79ea (patch) | |
| tree | 1fe7b221a0894d4be23ce6bc42a72c0915fb60ec | |
| parent | 6a148b1b876906cdea6ed74dc80789f8a3ea16e6 (diff) | |
Apply suggestions from code review
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
| -rw-r--r-- | doc/sphinx/introduction.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 30b8681d2c..1424b4f3e1 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -60,7 +60,7 @@ Nonetheless, the manual has some structure that is explained below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in seven +- The second part describes the proof engine. It is divided into several chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -69,8 +69,8 @@ Nonetheless, the manual has some structure that is explained below. Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that realize one or more steps of the proof are presented: we call them *tactics*. The legacy language to combine these tactics into complex proof - strategies is given in Chapter :ref:`ltac`. The new and experimental - language that is eventually going to replace Ltac is presented in + strategies is given in Chapter :ref:`ltac`. The currently experimental + language that will eventually replace Ltac is presented in Chapter :ref:`ltac2`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. Finally, the |SSR| proof language is presented in |