diff options
| author | Vincent Laporte | 2018-10-24 11:37:19 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-24 11:54:31 +0000 |
| commit | ac613856324317543828632eaeb77ccb575c2f8f (patch) | |
| tree | 06a46c2fef806ea6d3326957c7320a7dc52c12fd | |
| parent | a95c781dadd2b4aa5a6b715cfc7238e761a807fc (diff) | |
[Manual] Fix an example
The `Undo` command is not reliable.
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 9 |
1 files 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. |