9 files changed, 158 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13246.v b/test-suite/bugs/closed/bug_13246.v
new file mode 100644
index 0000000000..11f5baaaf4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13246.v
@@ -0,0 +1,69 @@
+Axiom _0: Prop.
+
+From Coq Require Export Morphisms Setoid Utf8.
+
+Class Equiv A := equiv: relation A.
+
+Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "■ P" (at level 20, right associativity).
+
+(** Define the scope *)
+Declare Scope bi_scope.
+Delimit Scope bi_scope with I.
+
+Structure bi :=
+  Bi { bi_car :> Type;
+       bi_entails : bi_car → bi_car → Prop;
+       bi_impl : bi_car → bi_car → bi_car;
+       bi_forall : ∀ A, (A → bi_car) → bi_car; }.
+
+Declare Instance bi_equiv `{PROP:bi} : Equiv (bi_car PROP).
+
+Arguments bi_car : simpl never.
+Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
+Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
+Arguments bi_forall {PROP _} _%I : simpl never, rename.
+
+Notation "P ⊢ Q" := (bi_entails P%I Q%I) .
+Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) .
+
+Infix "→" := bi_impl : bi_scope.
+Notation "∀ x .. y , P" :=
+  (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
+
+(* bug disappears if definitional class *)
+Class Plainly (PROP : bi) := { plainly : PROP -> PROP; }.
+Notation "■ P" := (plainly P) : bi_scope.
+
+Section S.
+  Context {I : Type} {PROP : bi} `(Plainly PROP).
+
+  Lemma plainly_forall `{Plainly PROP} {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊣⊢ ■ (∀ a, Ψ a).
+  Proof. Admitted.
+
+  Global Instance entails_proper :
+    Proper (equiv ==> equiv ==> iff) (bi_entails : relation PROP).
+  Proof. Admitted.
+
+  Global Instance impl_proper :
+    Proper (equiv ==> equiv ==> equiv) (@bi_impl PROP).
+  Proof. Admitted.
+
+  Global Instance forall_proper A :
+    Proper (pointwise_relation _ equiv ==> equiv) (@bi_forall PROP A).
+  Proof. Admitted.
+
+  Declare Instance PROP_Equivalence: Equivalence (@equiv PROP _).
+
+  Set Mangle Names.
+  Lemma foo (P : I -> PROP) K:
+    K ⊢ ∀ (j : I)
+          (_ : Prop) (* bug disappears if this is removed *)
+      , (∀ i0, ■ P i0) → P j.
+  Proof.
+    setoid_rewrite plainly_forall.
+    (* retype in case the tactic did some nonsense *)
+    match goal with |- ?T => let _ := type of T in idtac end.
+  Abort.
+End S.
diff --git a/test-suite/bugs/closed/bug_13249.v b/test-suite/bugs/closed/bug_13249.v
new file mode 100644
index 0000000000..06f7ddbd3a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13249.v
@@ -0,0 +1,9 @@
+Global Generalizable All Variables.
+
+Section test.
+  Context {A : Type}.
+  Context `{!foo A}.
+
+  Goal foo A.
+  Proof. assumption. Defined.
+End test.
diff --git a/test-suite/bugs/closed/bug_13300.v b/test-suite/bugs/closed/bug_13300.v
new file mode 100644
index 0000000000..e4fcd6dacc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13300.v
@@ -0,0 +1,7 @@
+Polymorphic Definition type := Type.
+
+Inductive bad : type := .
+
+Fail Check bad : Prop.
+Check bad : Set.
+(* lowered as much as possible *)
diff --git a/test-suite/bugs/closed/bug_13366.v b/test-suite/bugs/closed/bug_13366.v
new file mode 100644
index 0000000000..06918a9266
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13366.v
@@ -0,0 +1,5 @@
+Class Functor (F : Type -> Type) : Type :=
+  fmap : F nat.
+
+Fail Definition blah := sum fmap.
+(* used to be anomaly not an arity *)
diff --git a/test-suite/bugs/closed/bug_13453.v b/test-suite/bugs/closed/bug_13453.v
new file mode 100644
index 0000000000..4d0e435df7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13453.v
@@ -0,0 +1,6 @@
+Require Extraction.
+
+Primitive array := #array_type.
+
+Definition a : array nat := [| 0%nat | 0%nat |].
+Extraction a.
diff --git a/test-suite/bugs/closed/bug_7967.v b/test-suite/bugs/closed/bug_7967.v
index 2c8855fd54..987a820831 100644
--- a/test-suite/bugs/closed/bug_7967.v
+++ b/test-suite/bugs/closed/bug_7967.v
@@ -1,2 +1,6 @@
 Set Universe Polymorphism.
 Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A.
+
+(* A similar bug *)
+Context (C := ltac:(let y := constr:(Type) in exact nat)).
+Check C@{}.
diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v
index bb43edbe74..93ed94df39 100644
--- a/test-suite/bugs/closed/bug_9517.v
+++ b/test-suite/bugs/closed/bug_9517.v
@@ -2,6 +2,7 @@ Declare Custom Entry expr.
 Declare Custom Entry stmt.
 Notation "x" := x (in custom stmt, x ident).
 Notation "x" := x (in custom expr, x ident).
+Notation "'_'" := _ (in custom expr).
 
 Notation "1" := 1 (in custom expr).
 
diff --git a/test-suite/bugs/closed/bug_9809.v b/test-suite/bugs/closed/bug_9809.v
new file mode 100644
index 0000000000..4a7d2c7fac
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9809.v
@@ -0,0 +1,30 @@
+Section FreeMonad.
+
+  Variable S : Type.
+  Variable P : S -> Type.
+
+  Inductive FreeF A : Type :=
+  | retFree : A -> FreeF A
+  | opr     : forall s, (P s -> FreeF A) -> FreeF A.
+
+End FreeMonad.
+
+Section Fibonnacci.
+
+  Inductive gen_op := call_op : nat -> gen_op.
+  Definition gen_ty (op : gen_op) :=
+    match op with
+    | call_op _ => nat
+    end.
+
+  Fail Definition fib0 (n:nat) : FreeF gen_op gen_ty nat :=
+    match n  with
+    | 0
+    | 1 => retFree _ _ _ 1
+    | S (S k) =>
+      opr _ _ _ (call_op (S k))
+          (fun r1 => opr _ _ _ (call_op k)
+                      (fun r0 => retFree (* _ _ _ *) (r1 + r0)))
+    end.
+
+End Fibonnacci.
diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v
new file mode 100644
index 0000000000..ef526dcd7d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9971.v
@@ -0,0 +1,27 @@
+(* Test that it raises a normal error and not an anomaly *)
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+Arguments fst {A B} _.
+Arguments snd {A B} _.
+Arguments pair {A B} _ _.
+Record piis := { dep_types : Type; indep_args : dep_types -> Type }.
+Import EqNotations.
+Goal forall (id : Set) (V : id) (piiio : id -> piis)
+            (Z : {ridc : id & prod (dep_types (piiio ridc)) True})
+            (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}),
+    let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in
+    prod True (ida V (projT1 W)) ->
+    Z = existT _ V (pair (projT1 W) I) ->
+    ida (projT1 Z) (fst (projT2 Z)).
+  intros.
+  refine  (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+               H in
+              let v := I in
+              _);
+    refine (snd X).
+  Undo.
+Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+              H in
+             let v := I in
+             snd X).
+Abort.