diff options
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index b722b1af74..9362a7729e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -3,10 +3,6 @@ Ltac2 ===== -.. coqtop:: none - - From Ltac2 Require Import 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: @@ -88,6 +84,12 @@ which allows to ensure that Ltac2 satisfies the same equations as a generic ML with unspecified effects would do, e.g. function reduction is substitution by a value. +To import Ltac2, use the following command: + +.. coqtop:: in + + From Ltac2 Require Import Ltac2. + Type Syntax ~~~~~~~~~~~ |