Imported Upstream version 8.5~beta1+dfsg

1 files changed, 13 insertions, 12 deletions

diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake
index 47c77d23..76f400ef 100644
--- a/test-suite/ide/undo009.fake
+++ b/test-suite/ide/undo009.fake
@@ -4,17 +4,18 @@
 # Undoing declarations, interleaved with proof steps
 # new in 8.2 *)
 #
-INTERP Theorem k : O=O.
-INTERP assert True by trivial.
-INTERP Definition l := O.
-INTERP assert True by trivial.
-INTERP Definition m := O.
-REWIND 3
+ADD { Theorem k : O=O. }
+ADD here { assert True by trivial. }
+ADD { Definition l := O. }
+ADD { assert True by trivial. }
+ADD { Definition m := O. }
+QUERY { Show. }
+EDIT_AT here
 # <replay>
-INTERP Definition l := O.
-INTERP assert True by trivial.
-INTERP Definition m := O.
+ADD { Definition l := O. }
+ADD { assert True by trivial. }
+ADD { Definition m := O. }
 # <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }