7 files changed, 62 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_12348.v b/test-suite/bugs/closed/bug_12348.v
new file mode 100644
index 0000000000..93ba6f17e0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12348.v
@@ -0,0 +1,11 @@
+(* Was raising an anomaly before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := _ in
+      (fun n : nat => 0 : X) : _.
+
+(* Was raising an ill-typed instance error before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := true in
+      (fun n : nat => 0 : X) : _.
diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v
new file mode 100644
index 0000000000..9831a4d205
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13278.v
@@ -0,0 +1,15 @@
+Inductive even: nat -> Prop :=
+| evenB: even 0
+| evenS: forall n, even n -> even (S (S n)).
+
+Goal even 1 -> False.
+Proof.
+  refine (fun a => match a with end).
+Qed.
+
+Goal even 1 -> False.
+Proof.
+  refine (fun a => match a in even n
+                   return match n with 1 => False | _ => True end : Prop
+                   with evenB => I | evenS _ _ => I end).
+Qed.
diff --git a/test-suite/bugs/closed/bug_13363.v b/test-suite/bugs/closed/bug_13363.v
new file mode 100644
index 0000000000..cc11aa93b6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13363.v
@@ -0,0 +1,17 @@
+Axiom X : Type.       
+Axiom P : (X -> unit) -> Prop.
+
+Axiom F: unit -> unit.
+Axiom G : unit -> unit.
+
+Lemma Hyp ss':
+    P (fun y : X => ss') ->
+    P (fun y : X => G (F ss')).
+Admitted.
+
+Lemma bug : exists x, P x.
+Proof.
+intros.
+eexists (fun y : X => G _).
+eapply Hyp. cbn beta.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v
index 462a615d91..f3a19c2b89 100644
--- a/test-suite/bugs/closed/bug_3513.v
+++ b/test-suite/bugs/closed/bug_3513.v
@@ -13,7 +13,7 @@ Infix "|--"  := lentails (at level 79, no associativity).
 Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
 Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
 Section ILogic_Fun.
   Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v
index d667022e68..2d4d7d02cc 100644
--- a/test-suite/bugs/closed/bug_4095.v
+++ b/test-suite/bugs/closed/bug_4095.v
@@ -15,7 +15,7 @@ Infix "|--"  := lentails (at level 79, no associativity).
 Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
 Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
 Section ILogic_Fun.
   Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_5512.v b/test-suite/bugs/closed/bug_5512.v
new file mode 100644
index 0000000000..f885e31352
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5512.v
@@ -0,0 +1,10 @@
+(* Check that an anomaly is not raised *)
+(* It should however eventually succeed... *)
+Goal exists x, x.
+Proof.
+simple refine (ex_intro _ _ _).
+shelve.
+(* The failure is due to Type(u)<=Prop for u an arbitrary sort
+   variable being rejected *)
+Fail simple refine (_ _).
+Abort.
diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v
new file mode 100644
index 0000000000..72f612560b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6042.v
@@ -0,0 +1,7 @@
+Class C (n: nat) := T{x:True}.
+Generalizable All Variables.
+
+Fail Instance i : C n.
+
+Instance i : `(C n).
+Proof. repeat constructor. Defined.