Add several reproduction files for bugs.

11 files changed, 231 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
new file mode 100644
index 0000000000..4c9ba95ab6
--- /dev/null
+++ b/test-suite/bugs/opened/3509.v
@@ -0,0 +1,18 @@
+Lemma match_bool_fn b A B xT xF
+: match b as b return forall x : A, B b x with
+    | true => xT
+    | false => xF
+  end
+  = fun x : A => match b as b return B b x with
+                   | true => xT x
+                   | false => xF x
+                 end.
+admit.
+Defined.
+Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
+: (if b as b return B (if b then t else f) then F t else F f)
+  = F (if b then t else f).
+admit.
+Defined.
+Hint Rewrite match_bool_fn : matchdb.
+Hint Rewrite match_bool_comm_1 : matchdb.
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
new file mode 100644
index 0000000000..9e54893390
--- /dev/null
+++ b/test-suite/bugs/opened/3510.v
@@ -0,0 +1,34 @@
+Lemma match_option_fn T (b : option T) A B s n
+: match b as b return forall x : A, B b x with
+    | Some k => s k
+    | None => n
+  end
+  = fun x : A => match b as b return B b x with
+                   | Some k => s k x
+                   | None => n x
+                 end.
+admit.
+Defined.
+Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
+: match p as p return R match p with
+                          | Some k => s1 k
+                          | None => n1
+                        end
+                        match p as p return B match p with Some k => s1 k | None => n1 end with
+                          | Some k => s2 k
+                          | None => n2
+                        end with
+    | Some k => f (s1 k) (s2 k)
+    | None => f n1 n2
+  end
+  = f match p return A with
+        | Some k => s1 k
+        | None => n1
+      end
+      match p as p return B match p with Some k => s1 k | None => n1 end with
+        | Some k => s2 k
+        | None => n2
+      end.
+admit.
+Defined.
+Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
diff --git a/test-suite/bugs/opened/3554.v b/test-suite/bugs/opened/3554.v
new file mode 100644
index 0000000000..13a79cc840
--- /dev/null
+++ b/test-suite/bugs/opened/3554.v
@@ -0,0 +1 @@
+Example foo (f : forall {_ : Type}, Type) : Type.
diff --git a/test-suite/bugs/opened/3562.v b/test-suite/bugs/opened/3562.v
new file mode 100644
index 0000000000..cfbdd5554c
--- /dev/null
+++ b/test-suite/bugs/opened/3562.v
@@ -0,0 +1,2 @@
+Theorem t: True.
+destruct 0 as x.
diff --git a/test-suite/bugs/opened/3566.v b/test-suite/bugs/opened/3566.v
new file mode 100644
index 0000000000..e0075b8339
--- /dev/null
+++ b/test-suite/bugs/opened/3566.v
@@ -0,0 +1,21 @@
+Notation idmap := (fun x => x).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Delimit Scope path_scope with path.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := match p, q with idpath, idpath => idpath end.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x := match p with idpath => idpath end.
+Notation "p @ q" := (concat p q) (at level 20) : path_scope.
+Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope.
+Class IsEquiv {A B : Type} (f : A -> B) := {}.
+Axiom path_universe : forall {A B : Type} (f : A -> B) {feq : IsEquiv f}, (A = B).
+
+Definition Lift : Type@{i} -> Type@{j}
+  := Eval hnf in let lt := Type@{i} : Type@{j} in fun T => T.
+
+Definition lift {T} : T -> Lift T := fun x => x.
+
+Goal forall x y : Type, x = y.
+  intros.
+  pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @ (@path_universe _ _ (@lift y) (H0 y))^)))%path as H''.
diff --git a/test-suite/bugs/opened/3618.v b/test-suite/bugs/opened/3618.v
new file mode 100644
index 0000000000..cebfcc20ef
--- /dev/null
+++ b/test-suite/bugs/opened/3618.v
@@ -0,0 +1,100 @@
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+Definition concat {A} {x y z : A} : x = y -> y = z -> x = z. Admitted.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x. Admitted.
+Notation "p @ q" := (concat p q) (at level 20).
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y. Admitted.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y. Admitted.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : forall x, f (equiv_inv x) = x;
+  eissect : forall x, equiv_inv (f x) = x
+}.
+
+Class Contr_internal (A : Type).
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A)
+: IsTrunc n (x = y).
+Admitted.
+
+Class Funext.
+
+Instance isequiv_compose A B C f g `{IsEquiv A B f} `{IsEquiv B C g}
+  : IsEquiv (compose g f) | 1000.
+Admitted.
+
+Section IsEquivHomotopic.
+  Context (A B : Type) `(f : A -> B) `(g : A -> B) `{IsEquiv A B f} (h : forall x:A, f x = g x).
+  Let sect := (fun b:B => inverse (h (@equiv_inv _ _ f _ b)) @ @eisretr _ _ f _ b).
+  Let retr := (fun a:A => inverse (ap (@equiv_inv _ _ f _) (h a)) @ @eissect _ _ f _ a).
+  Global Instance isequiv_homotopic : IsEquiv g | 10000
+    := ( BuildIsEquiv _ _ g (@equiv_inv _ _ f _) sect retr).
+End IsEquivHomotopic.
+
+Instance trunc_succ A n `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000. Admitted.
+
+Global Instance trunc_forall A n `{P : A -> Type} `{forall a, IsTrunc n (P a)}
+  : IsTrunc n (forall a, P a) | 100.
+Admitted.
+
+Instance trunc_prod A B n `{IsTrunc n A} `{IsTrunc n B} : IsTrunc n (A * B) | 100.
+Admitted.
+
+Global Instance trunc_arrow n {A B : Type} `{IsTrunc n B} : IsTrunc n (A -> B) | 100.
+Admitted.
+
+Instance isequiv_pr1_contr {A} {P : A -> Type} `{forall a, IsTrunc minus_two (P a)}
+: IsEquiv (@projT1 A P) | 100.
+Admitted.
+
+Instance trunc_sigma n A `{P : A -> Type} `{IsTrunc n A} `{forall a, IsTrunc n (P a)}
+: IsTrunc n (sigT P) | 100.
+Admitted.
+
+Global Instance trunc_trunc `{Funext} A m n : IsTrunc (trunc_S n) (IsTrunc m A) | 0.
+Admitted.
+
+Definition BiInv {A B} (f : A -> B) : Type
+:= ( {g : B -> A & forall x, g (f x) = x} * {h : B -> A & forall x, f (h x) = x}).
+
+Global Instance isprop_biinv {A B} (f : A -> B) : IsTrunc (trunc_S minus_two) (BiInv f) | 0.
+Admitted.
+
+Instance isequiv_path {A B : Type} (p : A = B)
+: IsEquiv (transport (fun X:Type => X) p) | 0.
+Admitted.
+
+Class ReflectiveSubuniverse_internal :=
+  { inO_internal : Type -> Type ;
+    O : Type -> Type ;
+    O_unit : forall T, T -> O T }.
+
+Class ReflectiveSubuniverse :=
+  ReflectiveSubuniverse_wrap : Funext -> ReflectiveSubuniverse_internal.
+Global Existing Instance ReflectiveSubuniverse_wrap.
+
+Class inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) :=
+  isequiv_inO : inO_internal T.
+
+Global Instance hprop_inO {fs : Funext} {subU : ReflectiveSubuniverse} (T : Type) : IsTrunc (trunc_S minus_two) (inO T) .
+Admitted.
+
+Definition equiv_O_rectnd {fs : Funext} {subU : ReflectiveSubuniverse}
+           (P Q : Type) {Q_inO : inO_internal Q}
+: IsEquiv (fun f => compose f (O_unit P))
+:= _.
+
diff --git a/test-suite/bugs/opened/3625.v b/test-suite/bugs/opened/3625.v
new file mode 100644
index 0000000000..02110919b6
--- /dev/null
+++ b/test-suite/bugs/opened/3625.v
@@ -0,0 +1,7 @@
+Set Implicit Arguments.
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+
+Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
+  intros.
+  apply f_equal.
diff --git a/test-suite/bugs/opened/3626.v b/test-suite/bugs/opened/3626.v
new file mode 100644
index 0000000000..02110919b6
--- /dev/null
+++ b/test-suite/bugs/opened/3626.v
@@ -0,0 +1,7 @@
+Set Implicit Arguments.
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+
+Goal forall x y : prod Set Set, x.(@fst) = y.(@fst).
+  intros.
+  apply f_equal.
diff --git a/test-suite/bugs/opened/3628.v b/test-suite/bugs/opened/3628.v
new file mode 100644
index 0000000000..4001cf7c2b
--- /dev/null
+++ b/test-suite/bugs/opened/3628.v
@@ -0,0 +1,9 @@
+Module NonPrim.
+  Class AClass := { x : Set }.
+  Arguments x {AClass}.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Class AClass := { x : Set }.
+  Arguments x {AClass}.
+End Prim.
diff --git a/test-suite/bugs/opened/3655.v b/test-suite/bugs/opened/3655.v
new file mode 100644
index 0000000000..3ef112b7c7
--- /dev/null
+++ b/test-suite/bugs/opened/3655.v
@@ -0,0 +1,5 @@
+Ltac bar x := pose x.
+Tactic Notation "foo" open_constr(x) := bar x.
+Class baz := { baz' : Type }.
+Goal True.
+  foo baz'.
diff --git a/test-suite/bugs/opened/3660.v b/test-suite/bugs/opened/3660.v
new file mode 100644
index 0000000000..0ee56b5aea
--- /dev/null
+++ b/test-suite/bugs/opened/3660.v
@@ -0,0 +1,27 @@
+Generalizable All Variables.
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
+Open Scope function_scope.
+Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
+Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+Axiom IsHSet : Type -> Type.
+Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000.
+admit.
+Defined.
+Set Primitive Projections.
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
+Global Instance isequiv_ap_setT X Y : IsEquiv (@ap _ _ setT X Y).
+admit.
+Defined.
+Local Open Scope equiv_scope.
+Axiom equiv_path : forall (A B : Type) (p : A = B), A <~> B.
+Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))).
+  intros.
+  change (IsEquiv (equiv_path C D o @ap _ _ setT C D)).
+  apply @isequiv_compose; [ | admit ].
+  solve [ apply isequiv_ap_setT ].
+  Undo.
+  typeclasses eauto.