aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-05-27 11:43:10 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-05-28 13:50:43 +0200
commitc6714db203f60413523ebeaac86242a6e4cc05e3 (patch)
tree9ffe2cc129142180ff6373401b388f212ce21226
parent866c41b9720413e00194ba7addb9c4277e114890 (diff)
Test for 4159
-rw-r--r--test-suite/ide/univ.fake14
-rw-r--r--tools/fake_ide.ml4
2 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/ide/univ.fake b/test-suite/ide/univ.fake
new file mode 100644
index 000000000..90af8785a
--- /dev/null
+++ b/test-suite/ide/univ.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# jumping between broken proofs + interp error while fixing.
+# the error should note make the GUI unfocus the currently focused proof.
+
+# first proof
+ADD { Set Implicit Arguments. }
+ADD { Record dynamic := dyn { dyn_type : Type; dyn_value : dyn_type }. }
+ADD { Lemma dyn_inj_type : forall A1 A2 (x1:A1) (x2:A2), dyn x1 = dyn x2 -> A1 = A2. }
+ADD { Proof. }
+ADD { now intros A1 A2 x1 x2 [= e1 e2]. }
+ADD { Qed. }
+JOIN
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index c2b126687..d7a292f4c 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -257,6 +257,9 @@ let eval_print l coq =
| [ Tok(_,"WAIT") ] ->
let phrase = "Stm Wait." in
eval_call (query (phrase,tip_id())) coq
+ | [ Tok(_,"JOIN") ] ->
+ let phrase = "Stm JoinDocument." in
+ eval_call (query (phrase,tip_id())) coq
| [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
let to_id, _ = get_id id in
if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
@@ -273,6 +276,7 @@ let grammar =
; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
; Seq [Item (eat_rex "WAIT")]
+ ; Seq [Item (eat_rex "JOIN")]
; Seq [Item (eat_rex "GOALS")]
; Seq [Item (eat_rex "FAILGOALS")]
; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]