Add a bunch of reproduction files for bugs.

6 files changed, 188 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3681.v b/test-suite/bugs/opened/3681.v
new file mode 100644
index 0000000000..194113c6ed
--- /dev/null
+++ b/test-suite/bugs/opened/3681.v
@@ -0,0 +1,20 @@
+Module Type FOO.
+  Parameters P Q : Type -> Type.
+End FOO.
+
+Module Type BAR.
+  Declare Module Import foo : FOO.
+  Parameter f : forall A, P A -> Q A -> A.
+End BAR.
+
+Module Type BAZ.
+  Declare Module Export foo : FOO.
+  Parameter g : forall A, P A -> Q A -> A.
+End BAZ.
+
+Module BAR_FROM_BAZ (baz : BAZ) : BAR.
+  Import baz.
+  Module foo <: FOO := foo.
+  Import foo.
+  Definition f : forall A, P A -> Q A -> A := g.
+End BAR_FROM_BAZ.
diff --git a/test-suite/bugs/opened/3682.v b/test-suite/bugs/opened/3682.v
new file mode 100644
index 0000000000..71baf78cf2
--- /dev/null
+++ b/test-suite/bugs/opened/3682.v
@@ -0,0 +1,5 @@
+Class Foo.
+Definition bar `{Foo} (x : Set) := Set.
+Instance: Foo.
+Definition bar1 := bar nat.
+Fail Definition bar2 := bar $(admit)$.
diff --git a/test-suite/bugs/opened/3684.v b/test-suite/bugs/opened/3684.v
new file mode 100644
index 0000000000..e32a51223c
--- /dev/null
+++ b/test-suite/bugs/opened/3684.v
@@ -0,0 +1,2 @@
+Definition foo : Set.
+  Fail refine ($(abstract admit)$).
diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/opened/3685.v
new file mode 100644
index 0000000000..d647b5a83d
--- /dev/null
+++ b/test-suite/bugs/opened/3685.v
@@ -0,0 +1,74 @@
+Set Universe Polymorphism.
+Class Funext := { }.
+Delimit Scope category_scope with category.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Set Implicit Arguments.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d);
+    identity_of : forall s m, morphism_of s s m = morphism_of s s m }.
+Definition sub_pre_cat `{Funext} (P : PreCategory -> Type) : PreCategory.
+Proof.
+  exact (@Build_PreCategory PreCategory Functor).
+Defined.
+Definition opposite (C : PreCategory) : PreCategory.
+Proof.
+  exact (@Build_PreCategory C (fun s d => morphism C d s)).
+Defined.
+Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope.
+Definition prod (C D : PreCategory) : PreCategory.
+Proof.
+  refine (@Build_PreCategory
+            (C * D)%type
+            (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)).
+Defined.
+Local Infix "*" := prod : category_scope.
+Record NaturalTransformation C D (F G : Functor C D) := {}.
+Definition functor_category (C D : PreCategory) : PreCategory.
+Proof.
+  exact (@Build_PreCategory (Functor C D) (@NaturalTransformation C D)).
+Defined.
+Local Notation "C -> D" := (functor_category C D) : category_scope.
+Module Export PointwiseCore.
+  Local Open Scope category_scope.
+  Definition pointwise
+             (C C' : PreCategory)
+             (F : Functor C' C)
+             (D D' : PreCategory)
+             (G : Functor D D')
+  : Functor (C -> D) (C' -> D').
+  Proof.
+    refine (Build_Functor
+              (C -> D) (C' -> D')
+              _
+              _
+              _);
+    abstract admit.
+  Defined.
+End PointwiseCore.
+Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G.
+Local Open Scope category_scope.
+Module Success.
+  Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
+             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
+  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
+    := Eval cbv zeta in
+        let object_of := (fun CD => (((fst CD) -> (snd CD))))
+        in Build_Functor
+             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
+             object_of
+             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
+             (fun _ _ => @Pidentity_of _ _ _ _).
+End Success.
+Module Bad.
+  Include PointwiseCore.
+  Fail Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
+             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
+  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
+    := Eval cbv zeta in
+        let object_of := (fun CD => (((fst CD) -> (snd CD))))
+        in Build_Functor
+             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
+             object_of
+             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
+             (fun _ _ => @Pidentity_of _ _ _ _).
diff --git a/test-suite/bugs/opened/3686.v b/test-suite/bugs/opened/3686.v
new file mode 100644
index 0000000000..5f76fc9907
--- /dev/null
+++ b/test-suite/bugs/opened/3686.v
@@ -0,0 +1,61 @@
+Set Universe Polymorphism.
+Set Implicit Arguments.
+Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
+Bind Scope category_scope with PreCategory.
+Record Functor (C D : PreCategory) :=
+  { object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d);
+    identity_of : forall s m, morphism_of s s m = morphism_of s s m }.
+Definition sub_pre_cat (P : PreCategory -> Type) : PreCategory.
+Proof.
+  exact (@Build_PreCategory PreCategory Functor).
+Defined.
+Definition opposite (C : PreCategory) : PreCategory.
+Proof.
+  exact (@Build_PreCategory C (fun s d => morphism C d s)).
+Defined.
+Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope.
+Definition prod (C D : PreCategory) : PreCategory.
+Proof.
+  refine (@Build_PreCategory
+            (C * D)%type
+            (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)).
+Defined.
+Local Infix "*" := prod : category_scope.
+Axiom functor_category : PreCategory -> PreCategory -> PreCategory.
+Local Notation "C -> D" := (functor_category C D) : category_scope.
+Module Export PointwiseCore.
+  Definition pointwise
+             (C C' : PreCategory)
+             (F : Functor C' C)
+             (D D' : PreCategory)
+             (G : Functor D D')
+  : Functor (C -> D) (C' -> D').
+  Proof.
+    refine (Build_Functor
+              (C -> D) (C' -> D')
+              _
+              _
+              _);
+    abstract admit.
+  Defined.
+End PointwiseCore.
+Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G.
+Local Open Scope category_scope.
+Definition functor_uncurried (P : PreCategory -> Type)
+           (has_functor_categories : forall C D : @sub_pre_cat P, P (C -> D))
+: object (((@sub_pre_cat P)^op * (@sub_pre_cat P)) -> (@sub_pre_cat P)).
+Proof.
+  pose (let object_of := (fun CD => (((fst CD) -> (snd CD))))
+        in Build_Functor
+             ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P)
+             object_of
+             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
+             (fun _ _ => Pidentity_of _ _)) || fail "early".
+  Include PointwiseCore.
+  Fail pose (let object_of := (fun CD => (((fst CD) -> (snd CD))))
+        in Build_Functor
+             ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P)
+             object_of
+             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
+             (fun _ _ => Pidentity_of _ _)).
diff --git a/test-suite/bugs/opened/3692.v b/test-suite/bugs/opened/3692.v
new file mode 100644
index 0000000000..1a9e38b794
--- /dev/null
+++ b/test-suite/bugs/opened/3692.v
@@ -0,0 +1,26 @@
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Reserved Notation "x = y" (at level 70, no associativity).
+Reserved Notation "x * y" (at level 40, left associativity).
+Delimit Scope core_scope with core.
+Open Scope core_scope.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Global Set Primitive Projections.
+Global Set Implicit Arguments.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Generalizable Variables X A B f g n.
+Axiom path_prod' : forall {A B : Type} {x x' : A} {y y' : B}, (x = x') -> (y = y') -> ((x,y) = (x',y')).
+Definition functor_prod {A A' B B' : Type} (f:A->A') (g:B->B')
+: A * B -> A' * B'.
+  exact (fun z => (f (fst z), g (snd z))).
+Defined.
+Fail Definition isequiv_functor_prod `{IsEquiv A A' f} `{IsEquiv B B' g}
+: IsEquiv (functor_prod f g)
+  := @Build_IsEquiv
+       _ _ (functor_prod f g) (functor_prod f^-1 g^-1)
+       (fun z => path_prod' (@eisretr _ _ f _ (fst z)) (@eisretr _ _ g _ (snd z))).