From ed76ae4246e7d8fca79944b12b058d6bc3cd702b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 1 Aug 2018 12:40:21 +0200
Subject: [refman] Fixing two nested lemma errors.

---
 doc/sphinx/proof-engine/tactics.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index d55748d645..35c974e2e1 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -974,7 +974,7 @@ Managing the local context
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: reset all
 
          Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x.
            intros x H z y H0.
@@ -1098,7 +1098,7 @@ Managing the local context
 
    .. example::
 
-      .. coqtop:: all
+      .. coqtop:: reset all
 
          Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C.
            intros A B C H; decompose [and or] H.
-- 
cgit v1.2.3