diff options
Diffstat (limited to 'test-suite/ide/undo012.fake')
-rw-r--r-- | test-suite/ide/undo012.fake | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake index f9b29ca1..b3d1c6d5 100644 --- a/test-suite/ide/undo012.fake +++ b/test-suite/ide/undo012.fake @@ -2,25 +2,25 @@ # Run it via fake_ide # # Test backtracking in presence of nested proofs -# First, undoing the whole # -INTERP Lemma aa : True -> True /\ True. -INTERP intro H. -INTERP split. -INTERP Lemma bb : False -> False. -INTERP intro H. -INTERP apply H. -INTERP Qed. -INTERP apply H. -INTERP Lemma cc : False -> True. -INTERP intro H. -INTERP destruct H. -INTERP Qed. -INTERP apply H. -INTERP Qed. -REWIND 1 -# We should now be just before aa, without opened proofs -INTERPRAW Fail idtac. -INTERPRAW Fail Check aa. -INTERPRAW Fail Check bb. -INTERPRAW Fail Check cc. +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD { intro H. } +ADD { apply H. } +ADD { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } +ADD { Qed. } +QUERY { Show. } +ADD here { apply H. } +ADD { Qed. } +EDIT_AT here +# We should now be just before the Qed. +QUERY { Fail Check aa. } +QUERY { Check bb. } +QUERY { Check cc. } +ADD { Qed. } |