Imported Upstream version 8.5~beta1+dfsg

1 files changed, 43 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3439.v b/test-suite/bugs/closed/3439.v
new file mode 100644
index 00000000..bba6140f
--- /dev/null
+++ b/test-suite/bugs/closed/3439.v
@@ -0,0 +1,43 @@
+(* File reduced by coq-bug-finder from original input, then from 3154 lines to 149 lines, then from 89 lines to 55 lines, then from 44 lines to 20 lines *)
+Set Primitive Projections.
+Generalizable All Variables.
+Axiom IsHSet : Type -> Type.
+Existing Class IsHSet.
+Record PreCategory := { object :> Type }.
+Notation IsStrictCategory C := (IsHSet (object C)).
+Instance trunc_prod `{IsHSet A} `{IsHSet B} : IsHSet (A * B) | 100.
+admit.
+Defined.
+Typeclasses Transparent object.
+Definition prod (C D : PreCategory) : PreCategory := Build_PreCategory (Datatypes.prod C D).
+Global Instance isstrict_category_product `{IsStrictCategory C, IsStrictCategory D} : IsStrictCategory (prod C D).
+Proof.
+  typeclasses eauto.
+Defined.
+
+
+Set Typeclasses Debug.
+(* File reduced by coq-bug-finder from original input, then from 7425 lines to 154 lines, then from 116 lines to 20 lines *)
+Class Contr (A : Type) := { center : A }.
+Instance contr_unit : Contr unit | 0 := {| center := tt |}.
+Module non_prim.
+  Unset Primitive Projections.
+  Record PreCategory := { object :> Type }.
+  Lemma foo : Contr (object (@Build_PreCategory unit)).
+  Proof.
+    solve [ simpl; typeclasses eauto ] || fail "goal not solved".
+    Undo.
+    solve [ typeclasses eauto ].
+  Defined.
+End non_prim.
+
+Module prim.
+  Set Primitive Projections.
+  Record PreCategory := { object :> Type }.
+  Lemma foo : Contr (object (@Build_PreCategory unit)).
+  Proof.
+    solve [ simpl; typeclasses eauto ] || fail "goal not solved".
+    Undo.
+    solve [ typeclasses eauto ]. (*  Error: No applicable tactic. *)
+  Defined.
+End prim.
\ No newline at end of file