diff options
| author | Pierre-Marie Pédrot | 2019-12-23 15:17:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-23 15:17:27 +0100 |
| commit | 4bf98342425c20c062f0a861a658230668b06323 (patch) | |
| tree | 4cc398910bf5e56820330e9e13c9822399195c9c | |
| parent | 95fc326a64dd655e8e35af3cc64608d23c997de1 (diff) | |
| parent | 273586eca1f6372d3b633b7689b9cbb33d4e79ea (diff) | |
Merge PR #11324: [refman] Mention Ltac2 in intro.
Reviewed-by: jfehrle
| -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..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 six +- 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 @@ -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 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 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: |