diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-10 15:38:58 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-10 18:04:10 +0100 |
commit | 41845e6d4334eeaa7addf6b11f6cb4cda5a7f8cc (patch) | |
tree | 6f96af6235de9141185252369baa4acdbc4d28c5 /test-suite/ide | |
parent | cee357d2457295473dfe5ca4ebd8948bb7bca498 (diff) |
fake_ide: ported to spawn
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. } |