diff options
Diffstat (limited to 'test-suite/ide')
-rw-r--r-- | test-suite/ide/undo007.fake | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake deleted file mode 100644 index 7a1dc81e0..000000000 --- a/test-suite/ide/undo007.fake +++ /dev/null @@ -1,20 +0,0 @@ -# Script simulating a dialog between coqide and coqtop -ideslave -# Run it via fake_ide -# -# Undoing declarations, as first step -# new in 8.2 -# -ADD { Theorem d : O=O. } -ADD here { Definition e := O. } -ADD { Definition f := O. } - -# This is a bug in Stm undo, e is lost from master -EDIT_AT here -ADD { Definition f := O. } -ADD { assert True by trivial. } -ADD { exact (eq_refl e). } -ADD { Qed. } -# QUERY { Stm PrintDag. } -# QUERY { Stm Finish. } -QUERY { Print d. } -QUERY { Check e. } |