From 980ed3e2cda0a1aaa2a31509cae17b9c0adc5501 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 20 May 2008 12:10:10 +0000 Subject: 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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10951 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/ide/undo.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'test-suite/ide') 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. -- cgit v1.2.3