diff options
Diffstat (limited to 'test-suite/ide/undo008.fake')
-rw-r--r-- | test-suite/ide/undo008.fake | 20 |
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. } |