diff options
Diffstat (limited to 'test-suite/ide/undo013.fake')
-rw-r--r-- | test-suite/ide/undo013.fake | 44 |
1 files changed, 20 insertions, 24 deletions
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake index 3b1c61e6..f44156aa 100644 --- a/test-suite/ide/undo013.fake +++ b/test-suite/ide/undo013.fake @@ -2,30 +2,26 @@ # Run it via fake_ide # # Test backtracking in presence of nested proofs -# Second, trigger the full undo of an inner proof +# Second, trigger the undo of an inner proof # -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. -REWIND 2 -# We should now be just before "Lemma 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 here { destruct H. } +ADD { Qed. } +ADD { apply H. } +EDIT_AT here # <replay> -INTERP Lemma cc : False -> True. -INTERP intro H. -INTERP destruct H. -INTERP Qed. -INTERP apply H. +ADD { Qed. } +ADD { apply H. } # </replay> -INTERP Qed. -INTERPRAW Fail idtac. -INTERPRAW Check (aa,bb,cc). +ADD { Qed. } +QUERY { Fail idtac. } +QUERY { Check (aa,bb,cc). } |