From ac613856324317543828632eaeb77ccb575c2f8f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Oct 2018 11:37:19 +0000
Subject: [Manual] Fix an example

The `Undo` command is not reliable.
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index e976396950..70d17b1915 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -916,11 +916,8 @@ but also folds ``x`` in the goal.
      .. coqtop:: reset
 
         From Coq Require Import ssreflect.
-        Set Implicit Arguments.
-        Unset Strict Implicit.
-        Unset Printing Implicit Defensive.
 
-     .. coqtop:: all undo
+     .. coqtop:: all
 
         Lemma test x t (Hx : x = 3) : x + t = 4.
         set z := 3 in Hx.
@@ -929,6 +926,10 @@ If the localization also mentions the goal, then the result is the following one
 
   .. example::
 
+     .. coqtop:: reset
+
+        From Coq Require Import ssreflect.
+
      .. coqtop:: all
 
         Lemma test x t (Hx : x = 3) : x + t = 4.
-- 
cgit v1.2.3