3 files changed, 80 insertions, 0 deletions
diff --git a/test-suite/interactive/4289.v b/test-suite/interactive/4289.v
new file mode 100644
index 0000000000..610a509c9b
--- /dev/null
+++ b/test-suite/interactive/4289.v
@@ -0,0 +1,14 @@
+(* Checking backtracking with modules which used to fail due to an
+   hash-consing bug *)
+
+Module Type A.
+  Axiom B : nat.
+End A.
+Module C (a : A).
+  Include a.
+  Definition c : nat := B.
+End C.
+Back 4.
+Module C (a : A).
+  Include a.
+  Definition c : nat := B.
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
index 0d75d52a31..0d75d52a31 100755..100644
--- a/test-suite/interactive/ParalITP_smallproofs.v
+++ b/test-suite/interactive/ParalITP_smallproofs.v
diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
new file mode 100644
index 0000000000..31e3493768
--- /dev/null
+++ b/test-suite/interactive/proof_block.v
@@ -0,0 +1,66 @@
+Goal False /\ True.
+Proof.
+split.
+  idtac.
+  idtac.
+  exact I.
+idtac.
+idtac.
+exact I.
+Qed.
+
+Lemma baz :  (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split. { eexists. split. par: trivial. }
+trivial.
+Qed.
+
+Lemma baz1 :  (True /\ False) /\ True.
+Proof.
+split. { split. par: trivial. }
+trivial.
+Qed.
+
+Lemma foo : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  { idtac.
+    unshelve eexists.
+    { apply 3. }
+    { split.
+      { idtac. trivialx. }
+      { reflexivity. } } }
+  trivial.
+Qed.
+
+Lemma foo1 : False /\ True.
+Proof.
+split.
+  { exact I. }
+  { exact I. }
+Qed.
+
+Definition banana := true + 4. 
+
+Check banana.
+
+Lemma bar : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  - idtac.
+    unshelve eexists.
+    + apply 3.
+    + split.
+      * idtacx. trivial. 
+      * reflexivity.
+  - trivial.
+Qed.
+
+Lemma baz2 :  ((1=0 /\ False) /\ True) /\ False.
+Proof.
+split. split. split.
+ - solve [ auto ].
+ - solve [ trivial ].
+ - solve [ trivial ].
+ - exact 6.
+Qed.
+\ No newline at end of file