6 files changed, 110 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 91b8a4ed08..b9c27a2fcf 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-resiliency off -async-proofs-command-error-resiliency off" 2>&1; \
 	  if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
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/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/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.