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 /doc/sphinx/proof-engine | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
[refman] Mention Ltac2 in intro.
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: |