diff options
| author | Théo Zimmermann | 2020-02-25 10:06:28 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-25 10:06:28 +0100 |
| commit | 457ea1b8917844e1b955ce419ce08cd0bdc7ccc5 (patch) | |
| tree | a4bd3a06e7e0f5c7086dfe7c2f8b2ab63cbb69db | |
| parent | cb428dd8834747f6d5ea97b88bdef5a8f04495b8 (diff) | |
| parent | c322a90bce8bf5fac2fcd492cfb03ba8aa29013e (diff) | |
Merge PR #11675: Make it clear how to import Ltac2
Reviewed-by: Zimmi48
| -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 ~~~~~~~~~~~ |