aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/ide
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-10 15:38:58 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-10 18:04:10 +0100
commit41845e6d4334eeaa7addf6b11f6cb4cda5a7f8cc (patch)
tree6f96af6235de9141185252369baa4acdbc4d28c5 /test-suite/ide
parentcee357d2457295473dfe5ca4ebd8948bb7bca498 (diff)
fake_ide: ported to spawn
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. }