diff options
| author | Théo Zimmermann | 2019-12-22 12:28:27 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-12-22 15:13:37 +0100 |
| commit | 6a148b1b876906cdea6ed74dc80789f8a3ea16e6 (patch) | |
| tree | 9da9ebfca1cdf0354dbc1c78020f528f66bbb661 | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
[refman] Mention Ltac2 in intro.
| -rw-r--r-- | doc/sphinx/introduction.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 6 |
2 files changed, 8 insertions, 6 deletions
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index bcdf3277ad..30b8681d2c 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 six +- The second part describes the proof engine. It is divided in seven 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 @@ -68,8 +68,10 @@ Nonetheless, the manual has some structure that is explained below. proofs, do multiple proofs in parallel is explained in 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 language to combine these tactics into complex proof - strategies is given in Chapter :ref:`ltac`. Examples of tactics + *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 + Chapter :ref:`ltac2`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. Finally, the |SSR| proof language is presented in Chapter :ref:`thessreflectprooflanguage`. diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index cfdc70d50e..dd80b29bda 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1,12 +1,12 @@ .. _ltac2: +Ltac2 +===== + .. coqtop:: none From Ltac2 Require Import Ltac2. -Ltac2 -===== - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: |