9 files changed, 176 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 91b8a4ed08..d779d1f9a4 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -421,7 +421,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
 	@echo "TEST      $<"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on" 2>&1; \
+	  $(BIN)fake_ide $< "$(BIN)coqtop -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/bugs/closed/4644.v b/test-suite/bugs/closed/4644.v
new file mode 100644
index 0000000000..f09b27c2b1
--- /dev/null
+++ b/test-suite/bugs/closed/4644.v
@@ -0,0 +1,52 @@
+(* Testing a regression of unification in 8.5 in problems of the form
+   "match ?y with ... end = ?x args" *)
+
+Lemma foo : exists b, forall a, match a with tt => tt end = b a.
+Proof.
+eexists. intro.
+refine (_ : _ = match _ with tt => _ end).
+refine eq_refl.
+Qed.
+
+(**********************************************************************)
+
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Export Coq.Classes.Morphisms.
+Require Import Coq.Lists.List.
+
+Global Set Implicit Arguments.
+
+Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs))
+           ls
+  : P ls
+  := match ls with
+     | nil => N
+     | x::xs => C x xs
+     end.
+
+Axiom list_caset_Proper'
+  : forall {A P},
+    Proper (eq
+              ==> pointwise_relation _ (pointwise_relation _ eq)
+              ==> eq
+              ==> eq)
+           (@list_caset A (fun _ => P)).
+Goal forall (T T' : Set) (a3 : list T), exists y2, forall (a4 : T' -> bool),
+        match a3 with
+        | nil => 0
+        | (_ :: _)%list => 1
+        end = y2 a4.
+  clear; eexists; intros.
+  reflexivity. Undo.
+  Local Ltac t :=
+    lazymatch goal with
+    | [ |- match ?v with nil => ?N | cons x xs => @?C x xs end = _ :> ?P ]
+      => let T := type of v in
+         let A := match (eval hnf in T) with list ?A => A end in
+         refine (@list_caset_Proper' A P _ _ _ _ _ _ _ _ _
+                 : @list_caset A (fun _ => P) N C v = match _ with nil => _ | cons x xs => _ end)
+    end.
+  (etransitivity; [ t | reflexivity ]) || fail 0 "too early".
+  Undo.
+  t.
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
new file mode 100644
index 0000000000..ed44437861
--- /dev/null
+++ b/test-suite/bugs/closed/4782.v
@@ -0,0 +1,9 @@
+(* About typing of with bindings *)
+
+Record r : Type := mk_r { type : Type; cond : type -> Prop }.
+
+Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
+
+Goal p.
+Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
+ 
diff --git a/test-suite/bugs/closed/4787.v b/test-suite/bugs/closed/4787.v
new file mode 100644
index 0000000000..b586cba50f
--- /dev/null
+++ b/test-suite/bugs/closed/4787.v
@@ -0,0 +1,9 @@
+(* [Unset Bracketing Last Introduction Pattern] was not working *)
+
+Unset Bracketing Last Introduction Pattern.
+
+Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y.
+do 10 ((intros [] || intro); simpl); reflexivity.
+Qed.
+
+
diff --git a/test-suite/bugs/closed/4813.v b/test-suite/bugs/closed/4813.v
new file mode 100644
index 0000000000..5f8ea74c1a
--- /dev/null
+++ b/test-suite/bugs/closed/4813.v
@@ -0,0 +1,9 @@
+(* On the strength of "apply with" (see also #4782) *)
+
+Record ProverT := { Facts : Type }.
+Record ProverT_correct (P : ProverT) :=  { Valid : Facts P -> Prop ;
+                                           Valid_weaken : Valid = Valid }.
+Definition reflexivityValid (_ : unit) := True.
+Definition reflexivityProver_correct : ProverT_correct {| Facts := unit |}.
+Proof.
+    eapply Build_ProverT_correct with (Valid := reflexivityValid).
diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v
new file mode 100644
index 0000000000..86597c88fa
--- /dev/null
+++ b/test-suite/bugs/closed/4816.v
@@ -0,0 +1,17 @@
+Section foo.
+Polymorphic Universes A B.
+Fail Constraint A <= B.
+End foo.
+(* gives an anomaly Universe undefined *)
+
+Universes X Y.
+Section Foo.
+  Polymorphic Universes Z W.
+  Polymorphic Constraint W < Z.
+
+  Fail Definition bla := Type@{W}.
+  Polymorphic Definition bla := Type@{W}.
+  Section Bar.
+    Fail Constraint X <= Z.
+  End Bar.
+End Foo.
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v
new file mode 100644
index 0000000000..b75170179b
--- /dev/null
+++ b/test-suite/bugs/opened/4813.v
@@ -0,0 +1,5 @@
+(* An example one would like to see succeeding *)
+
+Record T := BT { t : Set }.
+Record U (x : T) := BU { u : t x -> Prop }.
+Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.
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
diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
new file mode 100644
index 0000000000..d5552695c4
--- /dev/null
+++ b/test-suite/success/ltacprof.v
@@ -0,0 +1,8 @@
+(** Some LtacProf tests *)
+
+Set Ltac Profiling.
+Ltac multi := (idtac + idtac).
+Goal True.
+  try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
+Admitted.
+Show Ltac Profile.