aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ide
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/ide')
-rw-r--r--test-suite/ide/undo007.fake20
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. }