20 files changed, 375 insertions, 2 deletions

diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
index d5e9ee5e..ea392055 100644
--- a/test-suite/ide/undo.v
+++ b/test-suite/ide/undo.v
@@ -3,8 +3,8 @@
 
 (* Undoing arbitrary commands, as first step *)
 
-Theorem a : O=O.
-Ltac f x := x.
+Theorem a : O=O. (* 2 *)
+Ltac f x := x. (* 1 * 3 *)
 assert True by trivial.
 trivial.
 Qed.
@@ -79,6 +79,7 @@ Definition q := O.
 Definition r := O.
 
 (* Bug 2082 : Follow the numbers *)
+(* Broken due to proof engine rewriting *)
 
 Variable A : Prop.
 Variable B : Prop.
diff --git a/test-suite/ide/undo001.fake b/test-suite/ide/undo001.fake
new file mode 100644
index 00000000..bbaea7e7
--- /dev/null
+++ b/test-suite/ide/undo001.fake
@@ -0,0 +1,10 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 1 between two global definitions
+#
+INTERP Definition foo := 0.
+INTERP Definition bar := 1.
+REWIND 1
+INTERPRAW Check foo.
+INTERPRAW Fail Check bar.
diff --git a/test-suite/ide/undo002.fake b/test-suite/ide/undo002.fake
new file mode 100644
index 00000000..b855b6ea
--- /dev/null
+++ b/test-suite/ide/undo002.fake
@@ -0,0 +1,10 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 2 before two global definitions
+#
+INTERP Definition foo := 0.
+INTERP Definition bar := 1.
+REWIND 2
+INTERPRAW Fail Check foo.
+INTERPRAW Fail Check bar.
diff --git a/test-suite/ide/undo003.fake b/test-suite/ide/undo003.fake
new file mode 100644
index 00000000..4c72e8dc
--- /dev/null
+++ b/test-suite/ide/undo003.fake
@@ -0,0 +1,8 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Simple backtrack by 0 should be a no-op
+#
+INTERP Definition foo := 0.
+REWIND 0
+INTERPRAW Check foo.
diff --git a/test-suite/ide/undo004.fake b/test-suite/ide/undo004.fake
new file mode 100644
index 00000000..c2ddfb8c
--- /dev/null
+++ b/test-suite/ide/undo004.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing arbitrary commands, as first step
+#
+INTERP Theorem a : O=O.
+INTERP Ltac f x := x.
+REWIND 1
+# <replay>
+INTERP Ltac f x := x.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo005.fake b/test-suite/ide/undo005.fake
new file mode 100644
index 00000000..525b9f2a
--- /dev/null
+++ b/test-suite/ide/undo005.fake
@@ -0,0 +1,15 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing arbitrary commands, as non-first step
+#
+INTERP Theorem b : O=O.
+INTERP assert True by trivial.
+INTERP Ltac g x := x.
+# <replay>
+REWIND 1
+# <\replay>
+INTERP Ltac g x := x.
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo006.fake b/test-suite/ide/undo006.fake
new file mode 100644
index 00000000..ed88bef5
--- /dev/null
+++ b/test-suite/ide/undo006.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as first step
+# Was bugged in 8.1
+#
+INTERP Theorem c : O=O.
+INTERP Inductive T : Type := I.
+REWIND 1
+# <replay>
+INTERP Inductive T : Type := I.
+# <\replay>
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo007.fake b/test-suite/ide/undo007.fake
new file mode 100644
index 00000000..87c06dbb
--- /dev/null
+++ b/test-suite/ide/undo007.fake
@@ -0,0 +1,17 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as first step
+# new in 8.2
+#
+INTERP Theorem d : O=O.
+INTERP Definition e := O.
+INTERP Definition f := O.
+REWIND 1
+# <replay>
+INTERP Definition f := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
+INTERPRAW Check e.
diff --git a/test-suite/ide/undo008.fake b/test-suite/ide/undo008.fake
new file mode 100644
index 00000000..1c46c1e8
--- /dev/null
+++ b/test-suite/ide/undo008.fake
@@ -0,0 +1,18 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, as non-first step
+# new in 8.2
+#
+INTERP Theorem h : O=O.
+INTERP assert True by trivial.
+INTERP Definition i := O.
+INTERP Definition j := O.
+REWIND 1
+# <replay>
+INTERP Definition j := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
+INTERPRAW Check i.
diff --git a/test-suite/ide/undo009.fake b/test-suite/ide/undo009.fake
new file mode 100644
index 00000000..47c77d23
--- /dev/null
+++ b/test-suite/ide/undo009.fake
@@ -0,0 +1,20 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, interleaved with proof steps
+# new in 8.2 *)
+#
+INTERP Theorem k : O=O.
+INTERP assert True by trivial.
+INTERP Definition l := O.
+INTERP assert True by trivial.
+INTERP Definition m := O.
+REWIND 3
+# <replay>
+INTERP Definition l := O.
+INTERP assert True by trivial.
+INTERP Definition m := O.
+# <\replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo010.fake b/test-suite/ide/undo010.fake
new file mode 100644
index 00000000..4fe9df98
--- /dev/null
+++ b/test-suite/ide/undo010.fake
@@ -0,0 +1,28 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Undoing declarations, interleaved with proof steps and commands *)
+# new in 8.2 *)
+#
+INTERP Theorem n : O=O.
+INTERP assert True by trivial.
+INTERP Definition o := O.
+INTERP Ltac h x := x.
+INTERP assert True by trivial.
+INTERP Focus.
+INTERP Definition p := O.
+REWIND 1
+REWIND 1
+REWIND 1
+REWIND 1
+REWIND 1
+# <replay>
+INTERP Definition o := O.
+INTERP Ltac h x := x.
+INTERP assert True by trivial.
+INTERP Focus.
+INTERP Definition p := O.
+# </replay>
+INTERP assert True by trivial.
+INTERP trivial.
+INTERP Qed.
diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake
new file mode 100644
index 00000000..cc85a764
--- /dev/null
+++ b/test-suite/ide/undo011.fake
@@ -0,0 +1,32 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Bug 2082
+# Broken due to proof engine rewriting
+#
+INTERP Variable A : Prop.
+INTERP Variable B : Prop.
+INTERP Axiom OR : A \/ B.
+INTERP Lemma MyLemma2 : True.
+INTERP proof.
+INTERP per cases of (A \/ B) by OR.
+INTERP suppose A.
+INTERP     then (1 = 1).
+INTERP     then H1 : thesis.
+INTERP     thus thesis by H1.
+INTERP suppose B.
+REWIND 1
+# <replay>
+INTERP suppose B.
+# </replay>
+REWIND 2
+# <replay>
+INTERP     thus thesis by H1.
+INTERP suppose B.
+# </replay>
+INTERP    then (1 = 1).
+INTERP    then H2 : thesis.
+INTERP    thus thesis by H2.
+INTERP end cases.
+INTERP end proof.
+INTERP Qed.
diff --git a/test-suite/ide/undo012.fake b/test-suite/ide/undo012.fake
new file mode 100644
index 00000000..f9b29ca1
--- /dev/null
+++ b/test-suite/ide/undo012.fake
@@ -0,0 +1,26 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# First, undoing the whole
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+REWIND 1
+# We should now be just before aa, without opened proofs
+INTERPRAW Fail idtac.
+INTERPRAW Fail Check aa.
+INTERPRAW Fail Check bb.
+INTERPRAW Fail Check cc.
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
new file mode 100644
index 00000000..3b1c61e6
--- /dev/null
+++ b/test-suite/ide/undo013.fake
@@ -0,0 +1,31 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Second, trigger the full undo of an inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+REWIND 2
+# We should now be just before "Lemma cc"
+# <replay>
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+INTERP Qed.
+INTERP apply H.
+# </replay>
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
new file mode 100644
index 00000000..5224b504
--- /dev/null
+++ b/test-suite/ide/undo014.fake
@@ -0,0 +1,26 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Third, undo inside an inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 1
+# <replay>
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
new file mode 100644
index 00000000..32e46ec9
--- /dev/null
+++ b/test-suite/ide/undo015.fake
@@ -0,0 +1,29 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Fourth, undo from an inner proof to a above proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 4
+# <replay>
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
new file mode 100644
index 00000000..2a6e512c
--- /dev/null
+++ b/test-suite/ide/undo016.fake
@@ -0,0 +1,34 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# Test backtracking in presence of nested proofs
+# Fifth, undo from an inner proof to a previous inner proof
+#
+INTERP Lemma aa : True -> True /\ True.
+INTERP intro H.
+INTERP split.
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+REWIND 6
+# We should be just before "Lemma bb"
+# <replay>
+INTERP Lemma bb : False -> False.
+INTERP intro H.
+INTERP apply H.
+INTERP Qed.
+INTERP apply H.
+INTERP Lemma cc : False -> True.
+INTERP intro H.
+INTERP destruct H.
+# </replay>
+INTERP Qed.
+INTERP apply H.
+INTERP Qed.
+INTERPRAW Fail idtac.
+INTERPRAW Check (aa,bb,cc).
diff --git a/test-suite/ide/undo017.fake b/test-suite/ide/undo017.fake
new file mode 100644
index 00000000..232360e9
--- /dev/null
+++ b/test-suite/ide/undo017.fake
@@ -0,0 +1,13 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing inside modules
+#
+INTERP Module M.
+INTERP Definition x := 0.
+INTERP End M.
+REWIND 1
+# <replay>
+INTERP End M.
+# </replay>
+INTERPRAW Check M.x.
diff --git a/test-suite/ide/undo018.fake b/test-suite/ide/undo018.fake
new file mode 100644
index 00000000..ef0945ab
--- /dev/null
+++ b/test-suite/ide/undo018.fake
@@ -0,0 +1,13 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing inside section
+#
+INTERP Section M.
+INTERP Definition x := 0.
+INTERP End M.
+REWIND 1
+# <replay>
+INTERP End M.
+# </replay>
+INTERPRAW Check x.
diff --git a/test-suite/ide/undo019.fake b/test-suite/ide/undo019.fake
new file mode 100644
index 00000000..70e70d7e
--- /dev/null
+++ b/test-suite/ide/undo019.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# bug #2569 : Undoing a focused subproof
+#
+INTERP Goal True.
+INTERP {
+INTERP exact I.
+INTERP }
+REWIND 1
+# <replay>
+INTERP }
+# </replay>
+INTERP Qed.