summaryrefslogtreecommitdiff
path: root/test-suite/ide/undo008.fake
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/ide/undo008.fake')
-rw-r--r--test-suite/ide/undo008.fake20
1 files changed, 10 insertions, 10 deletions
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
index 1c46c1e8..72cab7a3 100644
--- a/test-suite/ide/undo008.fake
+++ b/test-suite/ide/undo008.fake
@@ -4,15 +4,15 @@
# Undoing declarations, as non-first step
# new in 8.2
#
-INTERP Theorem h : O=O.
-INTERP assert True by trivial.
-INTERP Definition i := O.
-INTERP Definition j := O.
-REWIND 1
+ADD { Theorem h : O=O. }
+ADD { assert True by trivial. }
+ADD here { Definition i := O. }
+ADD { Definition j := O. }
+EDIT_AT here
# <replay>
-INTERP Definition j := O.
+ADD { Definition j := O. }
# <\replay>
-INTERP assert True by trivial.
-INTERP trivial.
-INTERP Qed.
-INTERPRAW Check i.
+ADD { assert True by trivial. }
+ADD { trivial. }
+ADD { Qed. }
+QUERY { Check i. }