diff options
Diffstat (limited to 'test-suite/ide/undo015.fake')
-rw-r--r-- | test-suite/ide/undo015.fake | 42 |
1 files changed, 21 insertions, 21 deletions
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake index 32e46ec9..ac17985a 100644 --- a/test-suite/ide/undo015.fake +++ b/test-suite/ide/undo015.fake @@ -4,26 +4,26 @@ # Test backtracking in presence of nested proofs # Fourth, undo from an inner proof to a above 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. -REWIND 4 +ADD { Lemma aa : True -> True /\ True. } +ADD { intro H. } +ADD { split. } +ADD { Lemma bb : False -> False. } +ADD { intro H. } +ADD { apply H. } +ADD here { Qed. } +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } +EDIT_AT here # <replay> -INTERP apply H. -INTERP Lemma cc : False -> True. -INTERP intro H. -INTERP destruct H. +ADD { apply H. } +ADD { Lemma cc : False -> True. } +ADD { intro H. } +ADD { destruct H. } # </replay> -INTERP Qed. -INTERP apply H. -INTERP Qed. -INTERPRAW Fail idtac. -INTERPRAW Check (aa,bb,cc). +ADD { Qed. } +ADD { apply H. } +ADD { Qed. } +QUERY { Fail idtac. } +QUERY { Check (aa,bb,cc). } |