From c322a90bce8bf5fac2fcd492cfb03ba8aa29013e Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Mon, 24 Feb 2020 20:14:00 +0000
Subject: Make it clear how to import Ltac2

---
 doc/sphinx/proof-engine/ltac2.rst | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'doc')

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
 ~~~~~~~~~~~
 
-- 
cgit v1.2.3