Make it clear how to import Ltac2

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
 ~~~~~~~~~~~