diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-20 12:10:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-20 12:10:10 +0000 |
| commit | 980ed3e2cda0a1aaa2a31509cae17b9c0adc5501 (patch) | |
| tree | c6242b40932470f9419ecac6cd96d517ddd4504f /test-suite/ide | |
| parent | c44946e4c81c6c3bf615b7b4c293f6721affb15a (diff) | |
Léger backtrack sur commit coqide précédent (si la commande à annuler
à potentiellement modifié l'état, on ne peut se contenter d'un Abort :
il faut revenir au dernier état connu).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10951 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/ide')
| -rw-r--r-- | test-suite/ide/undo.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v index 98913ac4e..a76817a87 100644 --- a/test-suite/ide/undo.v +++ b/test-suite/ide/undo.v @@ -3,7 +3,7 @@ (* Undoing arbitrary commands, as first step *) -Theorem a:True. +Theorem a : O=O. Set Printing All. assert True by trivial. trivial. @@ -11,7 +11,7 @@ Qed. (* Undoing arbitrary commands, as non-first step *) -Theorem a:True. +Theorem b : O=O. assert True by trivial. Set Printing All. assert True by trivial. @@ -21,7 +21,7 @@ Qed. (* Undoing declarations, as first step *) (* was bugged in 8.1 *) -Theorem a:True. +Theorem c : O=O. Inductive T : Type := I. trivial. Qed. @@ -29,9 +29,9 @@ Qed. (* Undoing declarations, as first step *) (* new in 8.2 *) -Theorem a:True. -Definition b:=O. -Definition c:=O. +Theorem d : O=O. +Definition e := O. +Definition f := O. assert True by trivial. trivial. Qed. @@ -39,10 +39,10 @@ Qed. (* Undoing declarations, as non-first step *) (* new in 8.2 *) -Theorem a:True. +Theorem h : O=O. assert True by trivial. -Definition b:=O. -Definition c:=O. +Definition i := O. +Definition j := O. assert True by trivial. trivial. Qed. @@ -50,11 +50,11 @@ Qed. (* Undoing declarations, interleaved with proof steps *) (* new in 8.2 *) -Theorem a:True. +Theorem k : O=O. assert True by trivial. -Definition b:=O. +Definition l := O. assert True by trivial. -Definition c:=O. +Definition m := O. assert True by trivial. trivial. Qed. @@ -62,13 +62,13 @@ Qed. (* Undoing declarations, interleaved with proof steps and commands *) (* new in 8.2 *) -Theorem a:True. +Theorem n : O=O. assert True by trivial. -Definition b:=O. +Definition o := O. Set Printing All. assert True by trivial. Focus. -Definition c:=O. +Definition p := O. assert True by trivial. trivial. Qed. |