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 /doc/sphinx/proof-engine | |
| parent | 95fc326a64dd655e8e35af3cc64608d23c997de1 (diff) | |
| parent | 273586eca1f6372d3b633b7689b9cbb33d4e79ea (diff) | |
Merge PR #11324: [refman] Mention Ltac2 in intro.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 6 |
1 files changed, 3 insertions, 3 deletions
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: |