Add many more cases to the test-suite

I'd add more, but I'm tired and it's late and I should sleep.  Maybe
I'll pick up at 3279 (working down) another day.

Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed,
even though it raises an anomaly.  So there's no way I can think of to
test it.  I've left it in the [opened] directory anyway.

32 files changed, 2404 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3283.v b/test-suite/bugs/opened/3283.v
new file mode 100644
index 000000000..3ab5416e8
--- /dev/null
+++ b/test-suite/bugs/opened/3283.v
@@ -0,0 +1,28 @@
+Notation "P |-- Q" := (@eq nat P Q) (at level 80, Q at level 41, no associativity) .
+Notation "x &&& y" := (plus x y) (at level 40, left associativity, y at next level) .
+Notation "'Ex' x , P " := (plus x P) (at level 65, x at level 99, P at level 80).
+
+(* Succeed *)
+Check _ |-- _ &&& _ -> _.
+Check _ |-- _ &&& (Ex _, _ ) -> _.
+Check _ |-- (_ &&& Ex _, _ ) -> _.
+
+(* Why does this fail? *)
+Fail Check _ |-- _ &&& Ex _, _  -> _.
+(* The command has indeed failed with message:
+=> Error: The term "Ex ?17, ?18" has type "nat"
+which should be Set, Prop or Type. *)
+
+(* Just in case something is strange with -> *)
+Notation "P ----> Q" := (P -> Q) (right associativity, at level 99, Q at next level).
+
+(* Succeed *)
+Check _ |-- _ &&& _ ----> _.
+Check _ |-- _ &&& (Ex _, _ )  ----> _.
+Check _ |-- (_ &&& Ex _, _ )  ----> _.
+
+(* Why does this fail? *)
+Fail Check _ |-- _ &&& Ex _, _  ----> _.
+(* The command has indeed failed with message:
+=> Error: The term "Ex ?31, ?32" has type "nat"
+which should be Set, Prop or Type.*)
diff --git a/test-suite/bugs/opened/3289.v b/test-suite/bugs/opened/3289.v
new file mode 100644
index 000000000..63453c5b8
--- /dev/null
+++ b/test-suite/bugs/opened/3289.v
@@ -0,0 +1,21 @@
+(* File reduced by coq-bug-finder from original input, then from 1829 lines to 37 lines, then from 47 lines to 18 lines *)
+
+Class Contr_internal (A : Type) :=
+  BuildContr { center : A ;
+               contr : (forall y : A, True) }.
+Class Contr A := Contr_is_contr : Contr_internal A.
+Inductive Unit : Set := tt.
+Instance contr_unit : Contr Unit | 0 :=
+  let x := {|
+        center := tt;
+        contr := fun t : Unit => I
+      |} in x. (* success *)
+
+Fail Instance contr_unit' : Contr Unit | 0 :=
+  {|
+    center := tt;
+    contr := fun t : Unit => I
+  |}.
+(* Error: Mismatched contexts while declaring instance:
+ Expected: (Contr_is_contr : Contr_internal _UNBOUND_REL_1)
+ Found:   tt  (fun t : Unit => I) *)
diff --git a/test-suite/bugs/opened/3291.v b/test-suite/bugs/opened/3291.v
new file mode 100644
index 000000000..4e1c2630e
--- /dev/null
+++ b/test-suite/bugs/opened/3291.v
@@ -0,0 +1,8 @@
+Require Import Setoid.
+
+Definition segv : forall x, (x = 0%nat) -> (forall (y : nat), (y < x)%nat -> nat) = forall (y : nat), (y < 0)%nat -> nat.
+intros x eq.
+assert (H : forall y, (y < x)%nat = (y < 0)%nat).
+rewrite -> eq. auto.
+Fail Timeout 1 setoid_rewrite <- H. (* The command has indeed failed with message:
+=> Stack overflow. *)
diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v
new file mode 100644
index 000000000..d871f5d20
--- /dev/null
+++ b/test-suite/bugs/opened/3295.v
@@ -0,0 +1,104 @@
+Require Export Morphisms Setoid.
+
+Class lops := lmk_ops {
+  car: Type;
+  weq: relation car
+}.
+
+Implicit Arguments car [].
+
+Coercion car: lops >-> Sortclass.
+
+Instance weq_Equivalence `{lops}: Equivalence weq.
+Proof.
+Admitted.
+
+Module lset.
+Canonical Structure lset_ops A := lmk_ops (list A) (fun h k => True).
+End lset.
+
+Class ops := mk_ops {
+  ob: Type;
+  mor: ob -> ob -> lops;
+  dot: forall n m p, mor n m -> mor m p -> mor n p
+}.
+Coercion mor: ops >-> Funclass.
+Implicit Arguments ob [].
+
+Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p).
+Proof.
+Admitted.
+
+Section s.
+
+Import lset.
+
+Context `{X:lops} {I: Type}.
+
+Axiom sup : forall (f: I -> X) (J : list I), X.
+
+Global Instance sup_weq: Proper (pointwise_relation _ weq ==> weq ==> weq) sup.
+Proof.
+Admitted.
+
+End s.
+
+Axiom ord : forall (n : nat), Type.
+Axiom seq : forall n, list (ord n).
+
+Infix "=="   := weq (at level 79).
+Infix "*" := (dot _ _ _)      (left associativity, at level 40).
+
+Notation "∑_ ( i ∈ l ) f" := (@sup (mor _ _) _ (fun i => f) l)
+  (at level 41, F at level 41, i, A at level 50).
+
+Axiom dotxsum : forall `{X : ops} I J n m p (f: I -> X m n) (x: X p m) y,
+  x * (∑_(i∈ J) f i) == y.
+
+Definition mx X n m := ord n -> ord m -> X.
+
+Section bsl.
+Context `{X : ops} {u: ob X}.
+Notation U := (car (@mor X u u)).
+
+Lemma toto n m p q (M : mx U n m) N (P : mx U p q) Q i j : ∑_(j0 ∈ seq m) M i j0 * (∑_(j1 ∈ seq p) N j0 j1 * P j1 j) == Q.
+Proof.
+  Fail setoid_rewrite dotxsum.
+  (* Toplevel input, characters 0-22:
+Error:
+Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints.
+Unable to satisfy the following constraints:
+UNDEFINED EVARS:
+ ?101==[X u n m p q M N P Q i j j0 |- U] (goal evar)
+ ?106==[X u n m p q M N P Q i j |- relation (X u u)] (internal placeholder)
+ ?107==[X u n m p q M N P Q i j |- relation (list (ord m))]
+         (internal placeholder)
+ ?108==[X u n m p q M N P Q i j (do_subrelation:=do_subrelation)
+         |- Proper (pointwise_relation (ord m) weq ==> ?107 ==> ?106) sup]
+         (internal placeholder)
+ ?109==[X u n m p q M N P Q i j |- ProperProxy ?107 (seq m)]
+         (internal placeholder)
+ ?110==[X u n m p q M N P Q i j |- relation (X u u)] (internal placeholder)
+ ?111==[X u n m p q M N P Q i j (do_subrelation:=do_subrelation)
+         |- Proper (?106 ==> ?110 ==> Basics.flip Basics.impl) weq]
+         (internal placeholder)
+ ?112==[X u n m p q M N P Q i j |- ProperProxy ?110 Q] (internal placeholder)UNIVERSES:
+ {} |= Top.14 <= Top.37
+        Top.25 <= Top.24
+        Top.25 <= Top.32
+
+ALGEBRAIC UNIVERSES:{}
+UNDEFINED UNIVERSES:METAS:
+ 470[y] := ?101 : car (?99 ?467 ?465)
+ 469[x] := M i _UNBOUND_REL_1 : car (?99 ?467 ?466)  [type is checked]
+ 468[f] := fun i : ?463 => N _UNBOUND_REL_2 i * P i j :
+ ?463 -> ?99 ?466 ?465  [type is checked]
+ 467[p] := u : ob ?99  [type is checked]
+ 466[m] := u : ob ?99  [type is checked]
+ 465[n] := u : ob ?99  [type is checked]
+ 464[J] := seq p : list ?463  [type is checked]
+ 463[I] := ord p : Type  [type is checked]
+ *)
+Abort.
+
+End bsl.
diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/opened/3298.v
new file mode 100644
index 000000000..bce7c3f23
--- /dev/null
+++ b/test-suite/bugs/opened/3298.v
@@ -0,0 +1,23 @@
+Module JGross.
+  Hint Extern 1 => match goal with |- match ?E with end => case E end.
+
+  Goal forall H : False, match H return Set with end.
+  Proof.
+    intros.
+    Fail solve [ eauto ]. (* No applicable tactic *)
+    admit.
+  Qed.
+End JGross.
+
+Section BenDelaware.
+  Hint Extern 0 => admit.
+  Goal forall (H : False), id (match H return Set with end).
+  Proof.
+    eauto.
+  Qed.
+  Goal forall (H : False), match H return Set with end.
+  Proof.
+    Fail solve [ eauto ] .
+    admit.
+  Qed.
+End BenDelaware.
diff --git a/test-suite/bugs/opened/3301.v b/test-suite/bugs/opened/3301.v
new file mode 100644
index 000000000..955cfc3aa
--- /dev/null
+++ b/test-suite/bugs/opened/3301.v
@@ -0,0 +1,120 @@
+Section Hurkens.
+
+Definition Type2 := Type.
+Definition Type1 := Type : Type2.
+
+(** Assumption of a retract from Type into Prop *)
+
+Variable down : Type1 -> Prop.
+Variable up : Prop -> Type1.
+
+Hypothesis back : forall A, up (down A) -> A.
+
+Hypothesis forth : forall A, A -> up (down A).
+
+Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A),
+      P (back A (forth A a)) -> P a.
+
+Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A),
+      P a -> P (back A (forth A a)).
+
+(** Proof *)
+
+Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop.
+Definition U : Type1 := V -> Prop.
+
+Definition sb (z:V) : V := fun A r a => r (z A r) a.
+Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)).
+Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x).
+Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x).
+Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))).
+Definition I (x:U) : Prop :=
+  (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False.
+
+Lemma Omega : forall i:U -> Prop, induct i -> up (i WF).
+Proof.
+intros i y.
+apply y.
+unfold le, WF, induct.
+apply forth.
+intros x H0.
+apply y.
+unfold sb, le', le.
+compute.
+apply backforth_r.
+exact H0.
+Qed.
+
+Lemma lemma1 : induct (fun u => down (I u)).
+Proof.
+unfold induct.
+intros x p.
+apply forth.
+intro q.
+generalize (q (fun u => down (I u)) p).
+intro r.
+apply back in r.
+apply r.
+intros i j.
+unfold le, sb, le', le in j |-.
+apply backforth in j.
+specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))).
+apply q.
+exact j.
+Qed.
+
+Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False.
+Proof.
+intro x.
+generalize (x (fun u => down (I u)) lemma1).
+intro r; apply back in r.
+apply r.
+intros i H0.
+apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))).
+unfold le, WF in H0.
+apply back in H0.
+exact H0.
+Qed.
+
+Theorem paradox : False.
+Proof.
+exact (lemma2 Omega).
+Qed.
+
+End Hurkens.
+
+Definition informative (x : bool) :=
+  match x with
+  | true => Type
+  | false => Prop
+  end.
+
+Definition depsort (T : Type) (x : bool) : informative x :=
+  match x with
+  | true => T
+  | false => True
+  end.
+
+(* The projection prop should not be definable *)
+Set Primitive Projections.
+Record Box (T : Type) : Prop := wrap {prop : T}.
+
+Definition down (x : Type) : Prop := Box x.
+Definition up (x : Prop) : Type := x.
+
+Definition back A : up (down A) -> A := @prop A.
+
+Definition forth A : A -> up (down A) := wrap A.
+
+Definition backforth (A:Type) (P:A->Type) (a:A) :
+      P (back A (forth A a)) -> P a := fun H => H.
+
+Definition backforth_r (A:Type) (P:A->Type) (a:A) :
+      P a -> P (back A (forth A a)) := fun H => H.
+
+Theorem pandora : False.
+apply (paradox down up back forth backforth backforth_r).
+Qed.
+
+Print Assumptions pandora.
+(* Closed under the global context *)
diff --git a/test-suite/bugs/opened/3309.v b/test-suite/bugs/opened/3309.v
new file mode 100644
index 000000000..90f2a29cb
--- /dev/null
+++ b/test-suite/bugs/opened/3309.v
@@ -0,0 +1,318 @@
+(* -*- coq-prog-args: ("-emacs" "-impredicative-set") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines *)
+Set Universe Polymorphism.
+Record sigT' {A} (P : A -> Type) := existT' { projT1' : A; projT2' : P projT1' }.
+Notation "{ x : A &' P }" := (sigT' (A := A) (fun x => P)) : type_scope.
+Arguments existT' {A} P _ _.
+Axiom admit : forall {T}, T.
+Notation paths := identity .
+
+Unset Automatic Introduction.
+
+Definition UU := Set.
+
+Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) .
+Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) .
+
+Definition ddualand { X Y P : UU } (xp : ( X -> P ) -> P ) ( yp : ( Y -> P ) -> P ) : ( dirprod X Y -> P ) -> P.
+Proof.
+  intros X Y P xp yp X0 .
+  set ( int1 := fun ypp : ( ( Y -> P ) -> P ) => fun x : X => yp ( fun y : Y => X0 ( dirprodpair x y) ) ) .
+  apply ( xp ( int1 yp ) ) .
+Defined .
+Definition weq ( X Y : UU )  : UU .
+intros; exact ( sigT' (fun f:X->Y => admit) ).
+Defined.
+Definition pr1weq ( X Y : UU):= @projT1' _ _ : weq X Y -> (X -> Y).
+Coercion pr1weq : weq >-> Funclass.
+
+Definition invweq { X Y : UU } ( w : weq X Y ) : weq Y X .
+admit.
+Defined.
+
+Definition hProp := sigT (fun X : Type => admit).
+
+Definition hProppair ( X : UU ) ( is : admit ) : hProp@{Set i}.
+intros; exact (existT (fun X : UU => admit ) X is ).
+Defined.
+Definition hProptoType := @projT1 _ _ : hProp -> Type .
+Coercion hProptoType: hProp >-> Sortclass.
+
+Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ).
+
+Definition ishinh ( X : UU ) : hProp := hProppair ( ishinh_UU X ) admit.
+
+Definition hinhfun { X Y : UU } ( f : X -> Y ) : ishinh_UU X -> ishinh_UU Y.
+intros X Y f; exact ( fun isx : ishinh X => fun P : _ =>  fun yp : Y -> P => isx P ( fun x : X => yp ( f x ) ) ).
+Defined.
+
+Definition hinhuniv { X : UU } { P : hProp } ( f : X -> P ) ( wit : ishinh_UU X ) : P.
+intros; exact (  wit P f ).
+Defined.
+
+Definition hinhand { X Y : UU } ( inx1 : ishinh_UU X ) ( iny1 : ishinh_UU Y) : ishinh ( dirprod X Y ).
+intros; exact ( fun P:_  => ddualand (inx1 P) (iny1 P)) .
+Defined.
+
+Definition UU' := Type.
+Definition hSet:= sigT (fun X : UU' => admit) .
+Definition hSetpair := existT (fun X : UU' => admit).
+Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type.
+Coercion pr1hSet: hSet >-> Sortclass.
+
+Definition hPropset : hSet := existT _ hProp admit .
+
+Definition hsubtypes ( X : UU ) : Type.
+intros; exact (X -> hProp ).
+Defined.
+Definition carrier { X : UU } ( A : hsubtypes X ) : Type.
+intros; exact (sigT A).
+Defined.
+Coercion carrier : hsubtypes >-> Sortclass.
+
+Definition subtypesdirprod { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) : hsubtypes ( dirprod X Y ).
+admit.
+Defined.
+
+Lemma weqsubtypesdirprod { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) : weq ( subtypesdirprod A B ) ( dirprod A B ) .
+  admit.
+Defined.
+
+Lemma ishinhsubtypesdirprod  { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) ( isa : ishinh A ) ( isb : ishinh B ) : ishinh ( subtypesdirprod A B ) .
+Proof .
+  intros .
+  apply ( hinhfun ( invweq ( weqsubtypesdirprod A B ) ) ) .
+  apply hinhand .
+  apply isa .
+  apply isb .
+Defined .
+
+Definition hrel ( X : UU ) : Type.
+intros; exact ( X -> X -> hProp).
+Defined.
+
+Definition iseqrel { X : UU } ( R : hrel X ) : Type.
+admit.
+Defined.
+
+Definition eqrel ( X : UU ) : Type.
+intros; exact ( sigT ( fun R : hrel X => iseqrel R ) ).
+Defined.
+Definition pr1eqrel ( X : UU ) : eqrel X -> ( X -> ( X -> hProp ) ) := @projT1 _ _ .
+Coercion pr1eqrel : eqrel >-> Funclass .
+
+Definition hreldirprod { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) : hrel ( dirprod X Y ) .
+admit.
+Defined.
+Set Printing Universes.
+Print hProp.
+Print ishinh_UU.
+Print hProppair.
+Definition iseqclass { X : UU } ( R : hrel X ) ( A : hsubtypes X ) : Type.
+intros; exact ( dirprod ( ishinh ( carrier A ) ) ( dirprod ( forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) )) .
+Defined.
+Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) ) ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) : iseqclass R A.
+intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact ax2.
+Defined.
+
+Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X }  : iseqclass R A -> ishinh ( carrier A ) .
+intros X R A; exact ( fun is : iseqclass R A =>  projT1 is ).
+Defined.
+
+Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) .
+Proof .
+  intros .
+  set ( XY := dirprod X Y ) .
+  set ( AB := subtypesdirprod A B ) .
+  set ( RQ := hreldirprod R Q ) .
+  set ( ax0 := ishinhsubtypesdirprod  A B ( eqax0 isa ) admit ) .
+  apply ( iseqclassconstr _ ax0 admit admit ) .
+Defined .
+
+Definition image { X Y : UU } ( f : X -> Y ) : Type.
+intros; exact ( sigT ( fun y : Y => admit ) ).
+Defined.
+Definition pr1image { X Y : UU } ( f : X -> Y ) : image f -> Y.
+intros X Y f; exact ( @projT1 _  ( fun y : Y => admit ) ).
+Defined.
+
+Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f.
+  admit.
+Defined.
+
+Definition setquot { X : UU } ( R : hrel X ) : Type.
+intros; exact ( sigT ( fun A : _ => iseqclass R A ) ).
+Defined.
+Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R.
+intros; exact (existT _ A is ).
+Defined.
+Definition pr1setquot { X : UU } ( R : hrel X ) : setquot R -> ( hsubtypes X ).
+intros X R.
+exact ( @projT1 _ ( fun A : _ => iseqclass R A ) ).
+Defined.
+Coercion pr1setquot : setquot >-> hsubtypes .
+
+Definition setquotinset { X : UU } ( R : hrel X ) : hSet.
+intros; exact ( hSetpair (setquot R) admit) .
+Defined.
+
+Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ).
+intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2 ( projT1 cd ) ) ( projT2 ( projT2 cd ) ) ) ).
+Defined.
+
+Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y ) := forall x x' x0 x0' : X , R x x' ->  R x0 x0' ->  paths ( f x x0 ) ( f x' x0' ) .
+
+Definition binop ( X : UU ) : Type.
+intros; exact ( X -> X -> X ).
+Defined.
+
+Definition setwithbinop : Type.
+exact (sigT ( fun X : hSet => binop X ) ).
+Defined.
+Definition pr1setwithbinop : setwithbinop -> hSet@{Set j}.
+unfold setwithbinop.
+exact ( @projT1 _ ( fun X : hSet@{Set j} => binop@{Set} X ) ).
+Defined.
+Coercion pr1setwithbinop : setwithbinop >-> hSet .
+
+Definition op { X : setwithbinop } : binop X.
+intros; exact ( projT2 X ).
+Defined.
+
+Definition subsetswithbinop { X : setwithbinop } : Type.
+admit.
+Defined.
+
+Definition carrierofasubsetwithbinop { X : setwithbinop } ( A : @subsetswithbinop X ) : setwithbinop .
+admit.
+Defined.
+
+Coercion carrierofasubsetwithbinop : subsetswithbinop >-> setwithbinop .
+
+Definition binopeqrel { X : setwithbinop } : Type.
+intros; exact (sigT ( fun R : eqrel X => admit ) ).
+Defined.
+Definition binopeqrelpair { X : setwithbinop } := existT ( fun R : eqrel X => admit ).
+Definition pr1binopeqrel ( X : setwithbinop ) : @binopeqrel X -> eqrel X.
+intros X; exact ( @projT1 _ ( fun R : eqrel X => admit ) ) .
+Defined.
+Coercion pr1binopeqrel : binopeqrel >-> eqrel .
+
+Definition setwithbinopdirprod ( X Y : setwithbinop ) : setwithbinop .
+admit.
+Defined.
+
+Definition monoid : Type.
+exact ( sigT ( fun X : setwithbinop => admit ) ).
+Defined.
+Definition monoidpair := existT ( fun X : setwithbinop => admit ) .
+Definition pr1monoid : monoid -> setwithbinop := @projT1 _ _ .
+Coercion pr1monoid : monoid >-> setwithbinop .
+
+Notation "x + y" := ( op x y ) : addmonoid_scope .
+
+Definition submonoids { X : monoid } : Type.
+admit.
+Defined.
+
+Definition submonoidstosubsetswithbinop ( X : monoid ) : @submonoids X -> @subsetswithbinop X.
+admit.
+Defined.
+Coercion  submonoidstosubsetswithbinop : submonoids >-> subsetswithbinop .
+
+Definition abmonoid : Type.
+exact (sigT ( fun X : setwithbinop => admit ) ).
+Defined.
+
+Definition abmonoidtomonoid : abmonoid -> monoid.
+exact (fun X : _ => monoidpair ( projT1 X ) admit ).
+Defined.
+Coercion abmonoidtomonoid : abmonoid >-> monoid .
+
+Definition subabmonoids { X : abmonoid } := @submonoids X .
+
+Definition carrierofsubabmonoid { X : abmonoid } ( A : @subabmonoids X ) : abmonoid .
+Proof .
+  intros .
+  unfold subabmonoids in A .
+  split with A .
+  admit.
+Defined .
+
+Coercion carrierofsubabmonoid : subabmonoids >-> abmonoid .
+
+Definition abmonoiddirprod ( X Y : abmonoid ) : abmonoid .
+Proof .
+  intros .
+  split with ( setwithbinopdirprod X Y ) .
+  admit.
+Defined .
+
+Open Scope addmonoid_scope .
+
+Definition eqrelabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : eqrel ( setwithbinopdirprod X A ).
+admit.
+Defined.
+
+Definition binopeqrelabmonoidfrac ( X : abmonoid ) ( A : @subabmonoids X ) : @binopeqrel ( abmonoiddirprod X A ).
+intros; exact ( @binopeqrelpair ( setwithbinopdirprod X A ) ( eqrelabmonoidfrac X A ) admit ).
+Defined.
+
+Theorem setquotuniv  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ) : Y .
+Proof.
+  intros.
+  apply ( pr1image ( fun x : c => f ( projT1 x ) ) ) .
+  apply ( @hinhuniv ( projT1 c ) ( hProppair _ admit ) ( prtoimage ( fun x : c => f ( projT1 x ) ) ) ) .
+  pose ( eqax0 ( projT2 c ) )  as h.
+  simpl in *.
+  Set Printing Universes.
+  exact h.
+Defined .
+
+Definition setquotuniv2  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R ) : Y .
+Proof.
+  intros .
+  set ( RR := hreldirprod R R ) .
+  apply (setquotuniv RR Y admit).
+  apply dirprodtosetquot.
+  apply dirprodpair.
+  exact c.
+  exact c0.
+Defined .
+
+Definition  setquotfun2  { X Y : UU } ( RX : hrel X ) ( RY : eqrel Y ) ( f : X -> X -> Y ) ( cx cx0 : setquot RX ) : setquot RY .
+Proof .
+  intros .
+  apply ( setquotuniv2 RX ( setquotinset RY ) admit admit admit admit ) .
+Defined .
+
+Definition quotrel  { X : UU } { R : hrel X } : hrel ( setquot R ).
+intros; exact ( setquotuniv2 R hPropset admit admit ).
+Defined.
+
+Definition setwithbinopquot { X : setwithbinop } ( R : @binopeqrel X ) : setwithbinop .
+Proof .
+  intros .
+  split with ( setquotinset R )  .
+  set ( qtmlt := setquotfun2 R R op ) .
+  simpl .
+  unfold binop .
+  apply qtmlt .
+Defined .
+
+Definition abmonoidquot { X : abmonoid } ( R : @binopeqrel X ) : abmonoid .
+Proof .
+  intros .
+  split with  ( setwithbinopquot R )  .
+  admit.
+Defined .
+
+Definition abmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : abmonoid.
+intros; exact ( @abmonoidquot (abmonoiddirprod X (@carrierofsubabmonoid X A)) ( binopeqrelabmonoidfrac X A ) ).
+Defined.
+
+Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) :  hrel (@setquot (setwithbinopdirprod X A) (eqrelabmonoidfrac X A)).
+intros; exact (@quotrel _ _).
+Defined.
+
+Fail Timeout 3 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
diff --git a/test-suite/bugs/opened/3310.v b/test-suite/bugs/opened/3310.v
new file mode 100644
index 000000000..ee9f8edfd
--- /dev/null
+++ b/test-suite/bugs/opened/3310.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+CoInductive stream A := cons { hd : A; tl : stream A }.
+
+CoFixpoint id {A} (s : stream A) := cons _ (hd s) (id (tl s)).
+
+Lemma id_spec : forall A (s : stream A), id s = s.
+Proof.
+intros A s.
+Fail Timeout 1 change (id s) with (cons _ (hd (id s)) (tl (id s))).
diff --git a/test-suite/bugs/opened/3311.v b/test-suite/bugs/opened/3311.v
new file mode 100644
index 000000000..1c66bc1e5
--- /dev/null
+++ b/test-suite/bugs/opened/3311.v
@@ -0,0 +1,10 @@
+Require Import Setoid.
+Axiom bar : True = False.
+Goal True.
+  Fail setoid_rewrite bar. (* Toplevel input, characters 15-33:
+Error:
+Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints.
+
+Could not find an instance for "subrelation eq (Basics.flip Basics.impl)".
+With the following constraints:
+?3 : "True" *)
diff --git a/test-suite/bugs/opened/3312.v b/test-suite/bugs/opened/3312.v
new file mode 100644
index 000000000..749921e2f
--- /dev/null
+++ b/test-suite/bugs/opened/3312.v
@@ -0,0 +1,5 @@
+Require Import Setoid.
+Axiom bar : 0 = 1.
+Goal 0 = 1.
+  Fail rewrite_strat bar. (* Toplevel input, characters 15-32:
+Error: Tactic failure:setoid rewrite failed: Nothing to rewrite. *)
diff --git a/test-suite/bugs/opened/3319.v b/test-suite/bugs/opened/3319.v
new file mode 100644
index 000000000..7851a08ea
--- /dev/null
+++ b/test-suite/bugs/opened/3319.v
@@ -0,0 +1,28 @@
+(* File reduced by coq-bug-finder from original input, then from 5353 lines to 4545 lines, then from 4513 lines to 4504 lines, then from 4515 lines to 4508 lines, then from 4519 lines to 132 lines, then from 111 lines to 66 lines, then from 68 lines to 35 lines *)
+Set Implicit Arguments.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a
+                 where "x = y" := (@paths _ x y) : type_scope.
+Record PreCategory := { obj :> Type; morphism : obj -> obj -> Type }.
+Record NotionOfStructure (X : PreCategory) :=
+  { structure :> X -> Type;
+    is_structure_homomorphism
+    : forall x y (f : morphism X x y) (a : structure x) (b : structure y), Type }.
+
+Section precategory.
+  Variable X : PreCategory.
+  Variable P : NotionOfStructure X.
+  Local Notation object := { x : X & P x }.
+  Record morphism' (xa yb : object) := {}.
+  Fail Lemma issig_morphism xa yb
+  : { f : morphism X (projT1 xa) (projT1 yb)
+    & is_structure_homomorphism _ _ _ f (projT2 xa) (projT2 yb) }
+    = morphism' xa yb. (* Toplevel input, characters 169-171:
+Error:
+In environment
+X : PreCategory
+P : NotionOfStructure X
+xa : {x : _ & ?26 x}
+yb : {x : _ & ?26 x}
+The term "xa" has type "{x : _ & ?26 x}" while it is expected to have type
+ "{x : X & P x}". *)
diff --git a/test-suite/bugs/opened/3322.v b/test-suite/bugs/opened/3322.v
new file mode 100644
index 000000000..67a68d55e
--- /dev/null
+++ b/test-suite/bugs/opened/3322.v
@@ -0,0 +1,23 @@
+(* File reduced by coq-bug-finder from original input, then from 11971 lines to 11753 lines, then from 7702 lines to 564 lines, then from 571 lines to 61 lines *)
+Set Asymmetric Patterns.
+Axiom admit : forall {T}, T.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
+           (pq : {p : (projT1 u) = (projT1 v) &  transport _ p (projT2 u) = (projT2 v)})
+: u = v.
+Proof.
+  destruct pq as [p q], u as [x y], v as [x' y']; simpl in *.
+  destruct p, q; simpl; reflexivity.
+Defined.
+Arguments path_sigma_uncurried : simpl never.
+Section opposite.
+  Let opposite_functor_involutive_helper
+    := @path_sigma_uncurried admit admit (existT _ admit admit) admit (existT _ admit admit).
+
+  Goal True.
+  Opaque path_sigma_uncurried.
+  simpl in *.
+  Transparent path_sigma_uncurried.
+  (* This command should fail with "Error: Failed to progress.", as it does in 8.4; the simpl never directive should prevent simpl from progressing *)
+  progress simpl in *.
diff --git a/test-suite/bugs/opened/3325.v b/test-suite/bugs/opened/3325.v
new file mode 100644
index 000000000..4c221dc7f
--- /dev/null
+++ b/test-suite/bugs/opened/3325.v
@@ -0,0 +1,28 @@
+Axiom SProp : Set.
+Axiom sp : SProp.
+
+(* If we hardcode valueType := nat, it goes through *)
+Class StateIs := {
+  valueType : Type;
+  stateIs : valueType -> SProp
+}.
+
+Instance NatStateIs : StateIs := {
+  valueType := nat;
+  stateIs := fun _ => sp
+}.
+
+Class LogicOps F := { land: F -> F }.
+Instance : LogicOps SProp. Admitted.
+Instance : LogicOps Prop. Admitted.
+
+Set Printing All.
+Parameter (n : nat).
+(* If this is a [Definition], the resolution goes through fine. *)
+Notation vn := (@stateIs _ n).
+Definition vn' := (@stateIs _ n).
+Definition GOOD : SProp :=
+  @land _ _ vn'.
+(* This doesn't resolve, if PropLogicOps is defined later than SPropLogicOps *)
+Fail Definition BAD : SProp :=
+  @land _ _ vn.
diff --git a/test-suite/bugs/opened/3326.v b/test-suite/bugs/opened/3326.v
new file mode 100644
index 000000000..f73117a2e
--- /dev/null
+++ b/test-suite/bugs/opened/3326.v
@@ -0,0 +1,18 @@
+Class ORDER A := Order {
+  LEQ : A -> A -> bool;
+  leqRefl: forall x, true = LEQ x x
+}.
+
+Section XXX.
+
+Variable A:Type.
+Variable (O:ORDER A).
+Definition aLeqRefl := @leqRefl _ O.
+
+Lemma OK : forall x, true = LEQ x x.
+  intros.
+  unfold LEQ.
+  destruct O.
+  clear.
+  Fail apply aLeqRefl. (* Toplevel input, characters 15-30:
+Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/opened/3329.v b/test-suite/bugs/opened/3329.v
new file mode 100644
index 000000000..efe1abcd2
--- /dev/null
+++ b/test-suite/bugs/opened/3329.v
@@ -0,0 +1,93 @@
+(* File reduced by coq-bug-finder from original input, then from 12095 lines to 869 lines, then from 792 lines to 504 lines, then from 487 lines to 353 lines, then from 258 lines to 174 lines, then from 164 lines to 132 lines, then from 129 lines to 99 lines *)
+Set Universe Polymorphism.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Notation "g 'o' f" := (compose g f).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) : Type := forall x:A, f x = g x.
+Hint Unfold pointwise_paths : typeclass_instances.
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+: forall x, f x = g x
+  := fun x => match h with idpath => idpath end.
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
+Class IsHSet (A : Type) := { _ : False }.
+Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+Record PreCategory :=
+  { object :> Type;
+    morphism : object -> object -> Type;
+    trunc_morphism : forall s d, IsHSet (morphism s d) }.
+
+Definition trunc_equiv `(f : A -> B) `{IsHSet A} `{IsEquiv A B f} : IsHSet B := admit.
+Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsHSet (P a)}
+: IsHSet (forall a, P a) | 100.
+Proof.
+  generalize dependent P.
+  intro P.
+  assert (f : forall a, P a) by admit.
+  assert (g : forall a, P a) by admit.
+  pose (@trunc_equiv (forall x : A, @paths (P x) (f x) (g x))
+                     (@paths (forall x : A, P x) f g)
+                     (@equiv_inv (@paths (forall x : A, P x) f g)
+                                 (forall x : A, @paths (P x) (f x) (g x))
+                                 (@apD10 A P f g) (@isequiv_apD10 H A P f g))).
+  admit.
+Defined.
+Record Functor (C D : PreCategory) := { object_of :> C -> D }.
+Definition identity C : Functor C C := Build_Functor C C admit.
+Notation "1" := (identity _) : functor_scope.
+Definition functor_category (C D : PreCategory) : PreCategory
+  := @Build_PreCategory (Functor C D) admit admit.
+Notation "C -> D" := (functor_category C D) : category_scope.
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Global Existing Instance iss.
+Definition set_cat `{Funext} : PreCategory :=
+  @Build_PreCategory hSet
+                     (fun x y => x -> y)
+                     _.
+
+Section hom_functor.
+  Context `{Funext}.
+  Variable C : PreCategory.
+
+  Local Notation obj_of c'c :=
+    (BuildhSet
+       (morphism
+          C
+          c'c
+          c'c)
+       admit).
+  Let hom_functor_morphism_of s's d'd (hf : morphism C s's d'd)
+  : morphism set_cat (obj_of s's) (obj_of d'd)
+    := admit.
+
+  Definition hom_functor : Functor C set_cat := admit.
+End hom_functor.
+Local Open Scope category_scope.
+Local Open Scope functor_scope.
+Context `{Funext}.
+Variable D : PreCategory.
+Set Printing Universes.
+Fail Check hom_functor D o 1.
+(* Toplevel input, characters 20-44:
+Error: Illegal application:
+The term "@set_cat" of type "(Funext -> PreCategory)%type"
+cannot be applied to the term
+ "H" : "Funext"
+This term has type "Funext" which should be coercible to
+"Funext". *)
+(* The command has indeed failed with message:
+=> Error: Illegal application:
+The term "@set_cat@{Top.345 Top.346 Top.331 Top.332 Top.337 Top.338 Top.339}"
+of type
+ "(Funext@{Top.346 Top.346 Top.331 Top.332 Top.346} -> PreCategory@{Top.345
+   Top.346})%type"
+cannot be applied to the term
+ "H@{Top.346 Top.330 Top.331 Top.332 Top.333}"
+   : "Funext@{Top.346 Top.330 Top.331 Top.332 Top.333}"
+This term has type "Funext@{Top.346 Top.330 Top.331 Top.332 Top.333}"
+which should be coercible to
+ "Funext@{Top.346 Top.346 Top.331 Top.332 Top.346}".
+*)
diff --git a/test-suite/bugs/opened/3330.v b/test-suite/bugs/opened/3330.v
new file mode 100644
index 000000000..face3b2d5
--- /dev/null
+++ b/test-suite/bugs/opened/3330.v
@@ -0,0 +1,1083 @@
+(* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *)
+Module Export HoTT_DOT_Overture.
+Module Export HoTT.
+Module Export Overture.
+
+Definition relation (A : Type) := A -> A -> Type.
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+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.
+
+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.
+
+Local Open Scope path_scope.
+
+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.
+
+Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p q) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p) (at level 3) : path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) : Type
+  := forall x:A, f x = g x.
+
+Hint Unfold pointwise_paths : typeclass_instances.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : f == g
+  := fun x => match h with idpath => 1 end.
+
+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) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Delimit Scope equiv_scope with equiv.
+
+Local Open Scope equiv_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+
+Class Contr_internal (A : Type) := BuildContr {
+  center : A ;
+  contr : (forall y : A, center = y)
+}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint nat_to_trunc_index (n : nat) : trunc_index
+  := match n with
+       | 0 => trunc_S (trunc_S minus_two)
+       | S n' => trunc_S (nat_to_trunc_index n')
+     end.
+
+Coercion nat_to_trunc_index : nat >-> 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.
+
+Notation IsHSet := (IsTrunc 0).
+
+Class Funext :=
+  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+
+Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
+  f == g -> f = g
+  :=
+  (@apD10 A P f g)^-1.
+
+End Overture.
+
+End HoTT.
+
+End HoTT_DOT_Overture.
+
+Module Export HoTT_DOT_categories_DOT_Category_DOT_Core.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Category.
+Module Export Core.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Delimit Scope morphism_scope with morphism.
+
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+
+Record PreCategory :=
+  Build_PreCategory' {
+      object :> Type;
+      morphism : object -> object -> Type;
+
+      identity : forall x, morphism x x;
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d'
+                              where "f 'o' g" := (compose f g);
+
+      associativity : forall x1 x2 x3 x4
+                             (m1 : morphism x1 x2)
+                             (m2 : morphism x2 x3)
+                             (m3 : morphism x3 x4),
+                        (m3 o m2) o m1 = m3 o (m2 o m1);
+
+      associativity_sym : forall x1 x2 x3 x4
+                                 (m1 : morphism x1 x2)
+                                 (m2 : morphism x2 x3)
+                                 (m3 : morphism x3 x4),
+                            m3 o (m2 o m1) = (m3 o m2) o m1;
+
+      left_identity : forall a b (f : morphism a b), identity b o f = f;
+      right_identity : forall a b (f : morphism a b), f o identity a = f;
+
+      identity_identity : forall x, identity x o identity x = identity x;
+
+      trunc_morphism : forall s d, IsHSet (morphism s d)
+    }.
+
+Bind Scope category_scope with PreCategory.
+
+Arguments identity [!C%category] x%object : rename.
+Arguments compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+Definition Build_PreCategory
+           object morphism compose identity
+           associativity left_identity right_identity
+  := @Build_PreCategory'
+       object
+       morphism
+       compose
+       identity
+       associativity
+       (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _))
+       left_identity
+       right_identity
+       (fun _ => left_identity _ _ _).
+
+Existing Instance trunc_morphism.
+
+Hint Resolve @left_identity @right_identity @associativity : category morphism.
+
+Module Export CategoryCoreNotations.
+
+  Infix "o" := compose : morphism_scope.
+End CategoryCoreNotations.
+End Core.
+
+End Category.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Category_DOT_Core.
+
+Module Export HoTT_DOT_types_DOT_Forall.
+
+Module Export HoTT.
+Module Export types.
+Module Export Forall.
+Generalizable Variables A B f g e n.
+
+Section AssumeFunext.
+
+Global Instance trunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)}
+  : IsTrunc n (forall a, P a) | 100.
+
+admit.
+Defined.
+End AssumeFunext.
+
+End Forall.
+
+End types.
+
+End HoTT.
+
+End HoTT_DOT_types_DOT_Forall.
+
+Module Export HoTT_DOT_types_DOT_Prod.
+
+Module Export HoTT.
+Module Export types.
+Module Export Prod.
+Local Open Scope path_scope.
+
+Definition path_prod_uncurried {A B : Type} (z z' : A * B)
+  (pq : (fst z = fst z') * (snd z = snd z'))
+  : (z = z')
+  := match pq with (p,q) =>
+       match z, z' return
+         (fst z = fst z') -> (snd z = snd z') -> (z = z') with
+         | (a,b), (a',b') => fun p q =>
+           match p, q with
+             idpath, idpath => 1
+           end
+       end p q
+     end.
+
+Definition path_prod {A B : Type} (z z' : A * B) :
+  (fst z = fst z') -> (snd z = snd z') -> (z = z')
+  := fun p q => path_prod_uncurried z z' (p,q).
+
+Definition path_prod' {A B : Type} {x x' : A} {y y' : B}
+  : (x = x') -> (y = y') -> ((x,y) = (x',y'))
+  := fun p q => path_prod (x,y) (x',y') p q.
+
+End Prod.
+
+End types.
+
+End HoTT.
+
+End HoTT_DOT_types_DOT_Prod.
+
+Module Export HoTT_DOT_categories_DOT_Functor_DOT_Core.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Functor.
+Module Export Core.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Delimit Scope functor_scope with functor.
+
+Local Open Scope morphism_scope.
+
+Section Functor.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Record Functor :=
+    {
+      object_of :> C -> D;
+      morphism_of : forall s d, morphism C s d
+                                -> morphism D (object_of s) (object_of d);
+      composition_of : forall s d d'
+                              (m1 : morphism C s d) (m2: morphism C d d'),
+                         morphism_of _ _ (m2 o m1)
+                         = (morphism_of _ _ m2) o (morphism_of _ _ m1);
+      identity_of : forall x, morphism_of _ _ (identity x)
+                              = identity (object_of x)
+    }.
+
+End Functor.
+Bind Scope functor_scope with Functor.
+
+Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+Module Export FunctorCoreNotations.
+
+  Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
+End FunctorCoreNotations.
+End Core.
+
+End Functor.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Functor_DOT_Core.
+
+Module Export HoTT_DOT_categories_DOT_Category_DOT_Morphisms.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Category.
+Module Export Morphisms.
+Set Universe Polymorphism.
+
+Local Open Scope morphism_scope.
+
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
+  {
+    morphism_inverse : morphism C d s;
+    left_inverse : morphism_inverse o m = identity _;
+    right_inverse : m o morphism_inverse = identity _
+  }.
+
+Class Isomorphic {C : PreCategory} s d :=
+  {
+    morphism_isomorphic :> morphism C s d;
+    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+  }.
+
+Module Export CategoryMorphismsNotations.
+
+  Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
+
+End CategoryMorphismsNotations.
+End Morphisms.
+
+End Category.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Category_DOT_Morphisms.
+
+Module Export HoTT_DOT_categories_DOT_Category_DOT_Dual.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Category.
+Module Export Dual.
+Set Universe Polymorphism.
+
+Local Open Scope morphism_scope.
+
+Section opposite.
+
+  Definition opposite (C : PreCategory) : PreCategory
+    := @Build_PreCategory'
+         C
+         (fun s d => morphism C d s)
+         (identity (C := C))
+         (fun _ _ _ m1 m2 => m2 o m1)
+         (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _)
+         (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _)
+         (fun _ _ => @right_identity _ _ _)
+         (fun _ _ => @left_identity _ _ _)
+         (@identity_identity C)
+         _.
+End opposite.
+
+Module Export CategoryDualNotations.
+
+  Notation "C ^op" := (opposite C) (at level 3) : category_scope.
+End CategoryDualNotations.
+End Dual.
+
+End Category.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Category_DOT_Dual.
+
+Module Export HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Functor.
+Module Export Composition.
+Module Export Core.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Local Open Scope morphism_scope.
+
+Section composition.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variable E : PreCategory.
+  Variable G : Functor D E.
+  Variable F : Functor C D.
+
+  Local Notation c_object_of c := (G (F c)) (only parsing).
+
+  Local Notation c_morphism_of m := (morphism_of G (morphism_of F m)) (only parsing).
+
+  Let compose_composition_of' s d d'
+      (m1 : morphism C s d) (m2 : morphism C d d')
+  : c_morphism_of (m2 o m1) = c_morphism_of m2 o c_morphism_of m1.
+admit.
+Defined.
+  Definition compose_composition_of s d d' m1 m2
+    := Eval cbv beta iota zeta delta
+            [compose_composition_of'] in
+        @compose_composition_of' s d d' m1 m2.
+  Let compose_identity_of' x
+  : c_morphism_of (identity x) = identity (c_object_of x).
+
+admit.
+Defined.
+  Definition compose_identity_of x
+    := Eval cbv beta iota zeta delta
+            [compose_identity_of'] in
+        @compose_identity_of' x.
+  Definition compose : Functor C E
+    := Build_Functor
+         C E
+         (fun c => G (F c))
+         (fun _ _ m => morphism_of G (morphism_of F m))
+         compose_composition_of
+         compose_identity_of.
+
+End composition.
+Module Export FunctorCompositionCoreNotations.
+
+  Infix "o" := compose : functor_scope.
+End FunctorCompositionCoreNotations.
+End Core.
+
+End Composition.
+
+End Functor.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Functor_DOT_Composition_DOT_Core.
+
+Module Export HoTT_DOT_categories_DOT_Functor_DOT_Dual.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Functor.
+Module Export Dual.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+
+Section opposite.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Definition opposite (F : Functor C D) : Functor C^op D^op
+    := Build_Functor (C^op) (D^op)
+                     (object_of F)
+                     (fun s d => morphism_of F (s := d) (d := s))
+                     (fun d' d s m1 m2 => composition_of F s d d' m2 m1)
+                     (identity_of F).
+
+End opposite.
+Module Export FunctorDualNotations.
+
+  Notation "F ^op" := (opposite F) : functor_scope.
+End FunctorDualNotations.
+End Dual.
+
+End Functor.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Functor_DOT_Dual.
+
+Module Export HoTT_DOT_categories_DOT_Functor_DOT_Identity.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Functor.
+Module Export Identity.
+Set Universe Polymorphism.
+
+Section identity.
+
+  Definition identity C : Functor C C
+    := Build_Functor C C
+                     (fun x => x)
+                     (fun _ _ x => x)
+                     (fun _ _ _ _ _ => idpath)
+                     (fun _ => idpath).
+End identity.
+Module Export FunctorIdentityNotations.
+
+  Notation "1" := (identity _) : functor_scope.
+End FunctorIdentityNotations.
+End Identity.
+
+End Functor.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Functor_DOT_Identity.
+
+Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core.
+
+Module Export HoTT.
+Module Export categories.
+Module Export NaturalTransformation.
+Module Export Core.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Local Open Scope morphism_scope.
+
+Section NaturalTransformation.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variables F G : Functor C D.
+
+  Record NaturalTransformation :=
+    Build_NaturalTransformation' {
+        components_of :> forall c, morphism D (F c) (G c);
+        commutes : forall s d (m : morphism C s d),
+                     components_of d o F _1 m = G _1 m o components_of s;
+
+        commutes_sym : forall s d (m : C.(morphism) s d),
+                         G _1 m o components_of s = components_of d o F _1 m
+      }.
+
+End NaturalTransformation.
+End Core.
+
+End NaturalTransformation.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Core.
+
+Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual.
+
+Module Export HoTT.
+Module Export categories.
+Module Export NaturalTransformation.
+Module Export Dual.
+Set Universe Polymorphism.
+
+Section opposite.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Definition opposite
+             (F G : Functor C D)
+             (T : NaturalTransformation F G)
+  : NaturalTransformation G^op F^op
+    := Build_NaturalTransformation' (G^op) (F^op)
+                                    (components_of T)
+                                    (fun s d => commutes_sym T d s)
+                                    (fun s d => commutes T d s).
+
+End opposite.
+
+End Dual.
+
+End NaturalTransformation.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Dual.
+
+Module Export HoTT_DOT_categories_DOT_Category_DOT_Strict.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Category.
+Module Export Strict.
+
+Export Category.Core.
+Set Universe Polymorphism.
+
+End Strict.
+
+End Category.
+
+End categories.
+
+End HoTT.
+
+End HoTT_DOT_categories_DOT_Category_DOT_Strict.
+
+Module Export HoTT.
+Module Export categories.
+Module Export Category.
+Module Export Prod.
+Set Universe Polymorphism.
+
+Local Open Scope morphism_scope.
+
+Section prod.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Definition prod : PreCategory.
+
+    refine (@Build_PreCategory
+              (C * D)%type
+              (fun s d => (morphism C (fst s) (fst d)
+                           * morphism D (snd s) (snd d))%type)
+              (fun x => (identity (fst x), identity (snd x)))
+              (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1))
+              _
+              _
+              _
+              _); admit.
+  Defined.
+End prod.
+Module Export CategoryProdNotations.
+
+  Infix "*" := prod : category_scope.
+End CategoryProdNotations.
+End Prod.
+
+End Category.
+
+End categories.
+
+End HoTT.
+
+Module Functor.
+Module Export Prod.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Local Open Scope morphism_scope.
+
+Section proj.
+
+  Context {C : PreCategory}.
+  Context {D : PreCategory}.
+  Definition fst : Functor (C * D) C
+    := Build_Functor (C * D) C
+                     (@fst _ _)
+                     (fun _ _ => @fst _ _)
+                     (fun _ _ _ _ _ => idpath)
+                     (fun _ => idpath).
+
+  Definition snd : Functor (C * D) D
+    := Build_Functor (C * D) D
+                     (@snd _ _)
+                     (fun _ _ => @snd _ _)
+                     (fun _ _ _ _ _ => idpath)
+                     (fun _ => idpath).
+
+End proj.
+
+Section prod.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variable D' : PreCategory.
+  Definition prod (F : Functor C D) (F' : Functor C D')
+  : Functor C (D * D')
+    := Build_Functor
+         C (D * D')
+         (fun c => (F c, F' c))
+         (fun s d m => (F _1 m, F' _1 m))
+         (fun _ _ _ _ _ => path_prod' (composition_of F _ _ _ _ _)
+                                      (composition_of F' _ _ _ _ _))
+         (fun _ => path_prod' (identity_of F _) (identity_of F' _)).
+
+End prod.
+Local Infix "*" := prod : functor_scope.
+
+Section pair.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variable C' : PreCategory.
+  Variable D' : PreCategory.
+  Variable F : Functor C D.
+  Variable F' : Functor C' D'.
+  Definition pair : Functor (C * C') (D * D')
+    := (F o fst) * (F' o snd).
+
+End pair.
+
+Module Export FunctorProdNotations.
+
+  Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : functor_scope.
+End FunctorProdNotations.
+End Prod.
+
+End Functor.
+
+Module Export HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.
+
+Module Export HoTT.
+Module categories.
+Module Export NaturalTransformation.
+Module Export Composition.
+Module Export Core.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Local Open Scope path_scope.
+
+Local Open Scope morphism_scope.
+
+Section composition.
+
+  Section compose.
+    Variable C : PreCategory.
+    Variable D : PreCategory.
+    Variables F F' F'' : Functor C D.
+    Variable T' : NaturalTransformation F' F''.
+
+    Variable T : NaturalTransformation F F'.
+    Local Notation CO c := (T' c o T c).
+
+    Definition compose_commutes s d (m : morphism C s d)
+    : CO d o morphism_of F m = morphism_of F'' m o CO s
+      := (associativity _ _ _ _ _ _ _ _)
+           @ ap (fun x => _ o x) (commutes T _ _ m)
+           @ (associativity_sym _ _ _ _ _ _ _ _)
+           @ ap (fun x => x o _) (commutes T' _ _ m)
+           @ (associativity _ _ _ _ _ _ _ _).
+
+    Definition compose_commutes_sym s d (m : morphism C s d)
+    : morphism_of F'' m o CO s = CO d o morphism_of F m
+      := (associativity_sym _ _ _ _ _ _ _ _)
+           @ ap (fun x => x o _) (commutes_sym T' _ _ m)
+           @ (associativity _ _ _ _ _ _ _ _)
+           @ ap (fun x => _ o x) (commutes_sym T _ _ m)
+           @ (associativity_sym _ _ _ _ _ _ _ _).
+
+    Definition compose
+    : NaturalTransformation F F''
+      := Build_NaturalTransformation' F F''
+                                      (fun c => CO c)
+                                      compose_commutes
+                                      compose_commutes_sym.
+
+  End compose.
+  End composition.
+Module Export NaturalTransformationCompositionCoreNotations.
+
+  Infix "o" := compose : natural_transformation_scope.
+End NaturalTransformationCompositionCoreNotations.
+End Core.
+
+End Composition.
+
+End NaturalTransformation.
+
+End categories.
+
+Set Universe Polymorphism.
+
+Section path_natural_transformation.
+
+  Context `{Funext}.
+  Variable C : PreCategory.
+
+  Variable D : PreCategory.
+  Variables F G : Functor C D.
+
+  Global Instance trunc_natural_transformation
+  : IsHSet (NaturalTransformation F G).
+
+admit.
+Defined.
+  Section path.
+
+    Variables T U : NaturalTransformation F G.
+
+    Lemma path'_natural_transformation
+    : components_of T = components_of U
+      -> T = U.
+
+admit.
+Defined.
+    Lemma path_natural_transformation
+    : components_of T == components_of U
+      -> T = U.
+
+    Proof.
+      intros.
+      apply path'_natural_transformation.
+      apply path_forall; assumption.
+    Qed.
+  End path.
+End path_natural_transformation.
+
+Ltac path_natural_transformation :=
+  repeat match goal with
+           | _ => intro
+           | _ => apply path_natural_transformation; simpl
+         end.
+
+Module Export Identity.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Local Open Scope morphism_scope.
+
+Local Open Scope path_scope.
+Section identity.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Section generalized.
+
+    Variables F G : Functor C D.
+    Hypothesis HO : object_of F = object_of G.
+    Hypothesis HM : transport (fun GO => forall s d,
+                                           morphism C s d
+                                           -> morphism D (GO s) (GO d))
+                              HO
+                              (morphism_of F)
+                    = morphism_of G.
+    Local Notation CO c := (transport (fun GO => morphism D (F c) (GO c))
+                                      HO
+                                      (identity (F c))).
+
+    Definition generalized_identity_commutes s d (m : morphism C s d)
+    : CO d o morphism_of F m = morphism_of G m o CO s.
+
+    Proof.
+      case HM.
+case HO.
+      exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^).
+    Defined.
+    Definition generalized_identity_commutes_sym s d (m : morphism C s d)
+    : morphism_of G m o CO s = CO d o morphism_of F m.
+
+admit.
+Defined.
+    Definition generalized_identity
+    : NaturalTransformation F G
+      := Build_NaturalTransformation'
+           F G
+           (fun c => CO c)
+           generalized_identity_commutes
+           generalized_identity_commutes_sym.
+
+  End generalized.
+  Definition identity (F : Functor C D)
+  : NaturalTransformation F F
+    := Eval simpl in @generalized_identity F F 1 1.
+
+End identity.
+Module Export NaturalTransformationIdentityNotations.
+
+  Notation "1" := (identity _) : natural_transformation_scope.
+End NaturalTransformationIdentityNotations.
+End Identity.
+
+Module Export Laws.
+Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories.
+Set Universe Polymorphism.
+
+Local Open Scope natural_transformation_scope.
+Section natural_transformation_identity.
+
+  Context `{fs : Funext}.
+  Variable C : PreCategory.
+
+  Variable D : PreCategory.
+
+  Lemma left_identity (F F' : Functor C D)
+        (T : NaturalTransformation F F')
+  : 1 o T = T.
+
+  Proof.
+    path_natural_transformation; auto with morphism.
+  Qed.
+
+  Lemma right_identity (F F' : Functor C D)
+        (T : NaturalTransformation F F')
+  : T o 1 = T.
+
+  Proof.
+    path_natural_transformation; auto with morphism.
+  Qed.
+End natural_transformation_identity.
+Section associativity.
+
+  Section nt.
+
+    Context `{fs : Funext}.
+    Definition associativity
+               C D F G H I
+               (V : @NaturalTransformation C D F G)
+               (U : @NaturalTransformation C D G H)
+               (T : @NaturalTransformation C D H I)
+    : (T o U) o V = T o (U o V).
+
+    Proof.
+      path_natural_transformation.
+      apply associativity.
+    Qed.
+  End nt.
+End associativity.
+End Laws.
+
+Module Export FunctorCategory.
+Module Export Core.
+Import HoTT_DOT_categories_DOT_NaturalTransformation_DOT_Composition_DOT_Core.HoTT.categories.
+Set Universe Polymorphism.
+
+Section functor_category.
+
+  Context `{Funext}.
+  Variable C : PreCategory.
+
+  Variable D : PreCategory.
+
+  Definition functor_category : PreCategory
+    := @Build_PreCategory (Functor C D)
+                          (@NaturalTransformation C D)
+                          (@identity C D)
+                          (@compose C D)
+                          (@associativity _ C D)
+                          (@left_identity _ C D)
+                          (@right_identity _ C D)
+                          _.
+
+End functor_category.
+Module Export FunctorCategoryCoreNotations.
+
+  Notation "C -> D" := (functor_category C D) : category_scope.
+End FunctorCategoryCoreNotations.
+End Core.
+
+End FunctorCategory.
+
+Module Export Morphisms.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+
+Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G :=
+  @Isomorphic (C -> D) F G.
+
+Module Export FunctorCategoryMorphismsNotations.
+
+  Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope.
+End FunctorCategoryMorphismsNotations.
+End Morphisms.
+
+Module Export HSet.
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+
+Global Existing Instance iss.
+End HSet.
+
+Module Export Core.
+Set Universe Polymorphism.
+
+Notation cat_of obj :=
+  (@Build_PreCategory obj
+                      (fun x y => x -> y)
+                      (fun _ x => x)
+                      (fun _ _ _ f g => f o g)%core
+                      (fun _ _ _ _ _ _ _ => idpath)
+                      (fun _ _ _ => idpath)
+                      (fun _ _ _ => idpath)
+                      _).
+
+Definition set_cat `{Funext} : PreCategory := cat_of hSet.
+Set Universe Polymorphism.
+
+Local Open Scope morphism_scope.
+
+Section hom_functor.
+
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Local Notation obj_of c'c :=
+    (BuildhSet
+       (morphism
+          C
+          (fst (c'c : object (C^op * C)))
+          (snd (c'c : object (C^op * C))))
+       _).
+
+  Let hom_functor_morphism_of s's d'd (hf : morphism (C^op * C) s's d'd)
+  : morphism set_cat (obj_of s's) (obj_of d'd)
+    := fun g => snd hf o g o fst hf.
+
+  Definition hom_functor : Functor (C^op * C) set_cat.
+
+    refine (Build_Functor (C^op * C) set_cat
+                          (fun c'c => obj_of c'c)
+                          hom_functor_morphism_of
+                          _
+                          _);
+    subst hom_functor_morphism_of;
+    simpl; admit.
+  Defined.
+End hom_functor.
+Set Universe Polymorphism.
+
+Import Category.Dual Functor.Dual.
+Import Category.Prod Functor.Prod.
+Import Functor.Composition.Core.
+Import Functor.Identity.
+Set Universe Polymorphism.
+
+Local Open Scope functor_scope.
+Local Open Scope natural_transformation_scope.
+Section Adjunction.
+
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variable F : Functor C D.
+  Variable G : Functor D C.
+  Let Adjunction_Type := Eval simpl in hom_functor D o (F^op, 1) <~=~> hom_functor C o (1, G).
+
+End Adjunction.
+Undo.
+
+  Record AdjunctionHom :=
+    {
+      mate_of : @NaturalIsomorphism
+                  H
+                  (Category.Prod.prod (Category.Dual.opposite C) D)
+                  (@Core.set_cat H)
+                  (@compose
+                     (Category.Prod.prod (Category.Dual.opposite C) D)
+                     (Category.Prod.prod (Category.Dual.opposite D) D)
+                     (@Core.set_cat H) (@hom_functor H D)
+                     (@pair (Category.Dual.opposite C)
+                            (Category.Dual.opposite D) D D
+                            (@opposite C D F) (identity D)))
+                  (@compose
+                     (Category.Prod.prod (Category.Dual.opposite C) D)
+                     (Category.Prod.prod (Category.Dual.opposite C) C)
+                     (@Core.set_cat H) (@hom_functor H C)
+                     (@pair (Category.Dual.opposite C)
+                            (Category.Dual.opposite C) D C
+                            (identity (Category.Dual.opposite C)) G))
+    }.
+Fail End Adjunction.
+(* Error: Illegal application:
+The term "NaturalIsomorphism" of type
+ "forall (H : Funext) (C D : PreCategory),
+  (C -> D)%category -> (C -> D)%category -> Type"
+cannot be applied to the terms
+ "H" : "Funext"
+ "(C ^op * D)%category" : "PreCategory"
+ "set_cat" : "PreCategory"
+ "hom_functor D o (F ^op, 1)" : "Functor (C ^op * D) set_cat"
+ "hom_functor C o (1, G)" : "Functor (C ^op * D) set_cat"
+The 5th term has type "Functor (C ^op * D) set_cat"
+which should be coercible to "object (C ^op * D -> set_cat)".
+*)
diff --git a/test-suite/bugs/opened/3331.v b/test-suite/bugs/opened/3331.v
new file mode 100644
index 000000000..07504aed7
--- /dev/null
+++ b/test-suite/bugs/opened/3331.v
@@ -0,0 +1,36 @@
+(* File reduced by coq-bug-finder from original input, then from 6303 lines to 66 lines, then from 63 lines to 36 lines *)
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y :> A" := (@paths A x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (x = y :>_) : type_scope.
+Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }.
+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) := H x y.
+Notation Contr := (IsTrunc minus_two).
+Section groupoid_category.
+  Variable X : Type.
+  Context `{H : IsTrunc (trunc_S (trunc_S (trunc_S minus_two))) X}.
+  Goal X -> True.
+    intro d.
+    pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as H'. (* success *)
+    clear H'.
+    compute in H.
+    change (forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)) in H.
+    assert (H' := H).
+    pose proof (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as X0. (* success *)
+    clear H' X0.
+    Fail pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* Toplevel input, characters 21-22:
+Error:
+Cannot infer this placeholder.
+Could not find an instance for "Contr (idpath = idpath)" in environment:
+
+X : Type
+H : forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)
+d : X *)
diff --git a/test-suite/bugs/opened/3332.v b/test-suite/bugs/opened/3332.v
new file mode 100644
index 000000000..275eaea5d
--- /dev/null
+++ b/test-suite/bugs/opened/3332.v
@@ -0,0 +1,6 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-time") -*- *)
+Definition foo : True.
+Proof.
+Abort. (* Toplevel input, characters 15-21:
+Anomaly: Backtrack.backto to a state with no vcs_backup. Please report. *)
+(* Anomaly: VernacAbort not handled by Stm. Please report. *)
diff --git a/test-suite/bugs/opened/3336.v b/test-suite/bugs/opened/3336.v
new file mode 100644
index 000000000..d469a13a3
--- /dev/null
+++ b/test-suite/bugs/opened/3336.v
@@ -0,0 +1,6 @@
+Require Import Setoid.
+Goal forall x y : Type, x = y -> x = y.
+intros x y H.
+Fail setoid_rewrite H.
+(* Toplevel input, characters 0-16:
+Anomaly: Uncaught exception Reduction.NotConvertible(_). Please report. *)
diff --git a/test-suite/bugs/opened/3337.v b/test-suite/bugs/opened/3337.v
new file mode 100644
index 000000000..06acd020a
--- /dev/null
+++ b/test-suite/bugs/opened/3337.v
@@ -0,0 +1,4 @@
+Require Import Setoid.
+Goal forall x y : Set, x = y -> x = y.
+intros x y H.
+Fail rewrite_strat subterms H.
diff --git a/test-suite/bugs/opened/3343.v b/test-suite/bugs/opened/3343.v
new file mode 100644
index 000000000..6c5a85f9c
--- /dev/null
+++ b/test-suite/bugs/opened/3343.v
@@ -0,0 +1,46 @@
+(* File reduced by coq-bug-finder from original input, then from 13699 lines to 656 lines, then from 584 lines to 200 lines *)
+Set Asymmetric Patterns.
+Require Export Coq.Lists.List.
+Export List.ListNotations.
+
+Record CFGV := { Terminal : Type; VarSym : Type }.
+
+Section Gram.
+  Context  {G : CFGV}.
+
+  Inductive  Pattern : (Terminal G) -> Type :=
+  | ptleaf : forall (T : Terminal G),
+               nat -> Pattern T
+  with Mixture : list (Terminal G) -> Type :=
+  | mtcons : forall {h: Terminal G}
+                    {tl: list (Terminal G)},
+               Pattern h -> Mixture tl -> Mixture (h::tl).
+
+  Variable vc : VarSym G.
+
+  Fixpoint pBVars {gs}  (p : Pattern gs) : (list nat) :=
+    match p with
+      | ptleaf _ _ => []
+    end
+  with mBVars {lgs} (pts : Mixture lgs) : (list nat) :=
+         match pts with
+           | mtcons _ _ _ tl =>  mBVars  tl
+         end.
+
+  Lemma mBndngVarsAsNth :
+    forall mp (m : @Mixture mp),
+      mBVars m = [2].
+  Proof.
+    intros.
+    induction m. progress simpl.
+  Admitted.
+End Gram.
+
+Lemma mBndngVarsAsNth' {G : CFGV} { vc  : VarSym G} :
+  forall mp (m : @Mixture G mp),
+    mBVars m = [2].
+Proof.
+  intros.
+  induction m.
+  Fail progress simpl.
+  (* simpl did nothing here, while it does something inside the section; this is probably a bug*)
diff --git a/test-suite/bugs/opened/3344.v b/test-suite/bugs/opened/3344.v
new file mode 100644
index 000000000..8255fd6cc
--- /dev/null
+++ b/test-suite/bugs/opened/3344.v
@@ -0,0 +1,58 @@
+(* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *)
+Require Import Coq.Sets.Ensembles.
+Require Import Coq.Strings.String.
+Global Set Implicit Arguments.
+Global Set Asymmetric Patterns.
+Ltac clearbodies := repeat match goal with | [ H := _ |- _ ] => clearbody H end.
+
+Inductive Comp : Type -> Type :=
+| Return : forall A, A -> Comp A
+| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B.
+Inductive computes_to : forall A, Comp A -> A -> Prop :=
+| ReturnComputes : forall A v, @computes_to A (Return v) v
+| BindComputes : forall A B comp_a f comp_a_value comp_b_value,
+                   @computes_to A comp_a comp_a_value
+                   -> @computes_to B (f comp_a_value) comp_b_value
+                   -> @computes_to B (Bind comp_a f) comp_b_value.
+
+Inductive is_computational : forall A, Comp A -> Prop :=
+| Return_is_computational : forall A (x : A), is_computational (Return x)
+| Bind_is_computational : forall A B (cA : Comp A) (f : A -> Comp B),
+                            is_computational cA
+                            -> (forall a,
+                                  @computes_to _ cA a -> is_computational (f a))
+                            -> is_computational (Bind cA f).
+Theorem is_computational_inv A (c : Comp A)
+: is_computational c
+  -> match c with
+       | Return _ _ => True
+       | Bind _ _ x f => is_computational x
+                         /\ forall v, computes_to x v
+                                      -> is_computational (f v)
+     end.
+  admit.
+Defined.
+Fixpoint is_computational_unique_val A (c : Comp A) {struct c}
+: is_computational c -> { a | unique (computes_to c) a }.
+Proof.
+  refine match c as c return is_computational c -> { a | unique (computes_to c) a } with
+           | Return T x => fun _ => exist (unique (computes_to (Return x)))
+                                          x
+                                          _
+           | Bind _ _ x f
+             => fun H
+                => let H' := is_computational_inv H in
+                   let xv := @is_computational_unique_val _ _ (proj1 H') in
+                   let fxv := @is_computational_unique_val _ _ (proj2 H' _ (proj1 (proj2_sig xv))) in
+                   exist (unique (computes_to _))
+                         (proj1_sig fxv)
+                         _
+         end;
+  clearbodies;
+  clear is_computational_unique_val;
+  clear;
+  first [ abstract admit
+        | abstract admit ].
+(* [Fail] does not catch the anomaly *)
+Defined.
+(* Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/3345.v
new file mode 100644
index 000000000..b61174a86
--- /dev/null
+++ b/test-suite/bugs/opened/3345.v
@@ -0,0 +1,144 @@
+(* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *)
+Global Set Implicit Arguments.
+Require Import Coq.Lists.List Program.
+Section IndexBound.
+  Context {A : Set}.
+  Class IndexBound (a : A) (Bound : list A) :=
+    { ibound :> nat;
+      boundi : nth_error Bound ibound = Some a}.
+  Global Arguments ibound [a Bound] _ .
+  Global Arguments boundi [a Bound] _.
+  Record BoundedIndex (Bound : list A) := { bindex :> A; indexb :> IndexBound bindex Bound }.
+End IndexBound.
+Context {A : Type} {C : Set}.
+Variable (projAC : A -> C).
+Lemma None_neq_Some
+: forall (AnyT AnyT' : Type) (a : AnyT),
+    None = Some a -> AnyT'.
+  admit.
+Defined.
+Program Definition nth_Bounded'
+           (Bound : list A)
+           (c : C)
+           (a_opt : option A)
+           (nth_n : option_map projAC a_opt = Some c)
+: A := match a_opt as x
+             return (option_map projAC x = Some c) -> A with
+         | Some a => fun _ => a
+         | None => fun f : None = Some _ => !
+       end nth_n.
+Lemma nth_error_map :
+  forall n As c_opt,
+    nth_error (map projAC As) n = c_opt
+    -> option_map projAC (nth_error As n) = c_opt.
+  admit.
+Defined.
+Definition nth_Bounded
+           (Bound : list A)
+           (idx : BoundedIndex (map projAC Bound))
+: A := nth_Bounded' Bound (nth_error Bound (ibound idx))
+                    (nth_error_map _ _ (boundi idx)).
+Program Definition nth_Bounded_ind2
+        (P : forall As, BoundedIndex (map projAC As)
+                        -> BoundedIndex (map projAC As)
+                        -> A -> A -> Prop)
+: forall (Bound : list A)
+         (idx : BoundedIndex (map projAC Bound))
+         (idx' : BoundedIndex (map projAC Bound)),
+    match nth_error Bound (ibound idx), nth_error Bound (ibound idx') with
+      | Some a, Some a' => P Bound idx idx' a a'
+      | _, _ => True
+    end
+    -> P Bound idx idx' (nth_Bounded _ idx) (nth_Bounded _ idx'):=
+  fun Bound idx idx' =>
+    match (nth_error Bound (ibound idx)) as e, (nth_error Bound (ibound idx')) as e'
+          return
+          (forall (f : option_map _ e = Some (bindex idx))
+                  (f' : option_map _ e' = Some (bindex idx')),
+             (match e, e' with
+                | Some a, Some a' => P Bound idx idx' a a'
+                | _, _ => True
+              end)
+             -> P Bound idx idx'
+                  (match e as e'' return
+                         option_map _ e'' = Some (bindex idx)
+                         -> A
+                   with
+                     | Some a => fun _ => a
+                     | _ => fun f => _
+                   end f)
+                  (match e' as e'' return
+                         option_map _ e'' = Some (bindex idx')
+                         -> A
+                   with
+                     | Some a => fun _ => a
+                     | _ => fun f => _
+                   end f')) with
+      | Some a, Some a' => fun _ _ H => _
+      | _, _ => fun f => _
+    end (nth_error_map _ _ (boundi idx))
+        (nth_error_map _ _ (boundi idx')).
+
+Lemma nth_Bounded_eq
+: forall (Bound : list A)
+         (idx idx' : BoundedIndex (map projAC Bound)),
+    ibound idx = ibound idx'
+    -> nth_Bounded Bound idx = nth_Bounded Bound idx'.
+Proof.
+  intros.
+  eapply nth_Bounded_ind2 with (idx := idx) (idx' := idx').
+  simpl.
+  (* The [case_eq] should not Fail.  More importantly, [Fail case_eq ...] should succeed if [case_eq ...] fails.  It doesn't!!!  So I resort to [Fail Fail try (case_eq ...)]. *)
+  Fail Fail try (case_eq (nth_error Bound (ibound idx'))).
+(* Toplevel input, characters 15-54:
+In nested Ltac calls to "case_eq" and "pattern x at - 1", last call failed.
+Error: The abstracted term
+"fun e : Exc A =>
+ forall e0 : nth_error Bound (ibound idx') = e,
+ match
+   nth_error Bound (ibound idx) as anonymous'0
+   return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop)
+ with
+ | Some a =>
+     match
+       e as anonymous'
+       return
+         (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop)
+     with
+     | Some a' =>
+         fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) =>
+         a = a'
+     | None =>
+         fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) =>
+         True
+     end
+ | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True
+ end eq_refl e0" is not well typed.
+Illegal application:
+The term
+ "match
+    nth_error Bound (ibound idx) as anonymous'0
+    return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop)
+  with
+  | Some a =>
+      match
+        e as anonymous'
+        return
+          (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop)
+      with
+      | Some a' =>
+          fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) =>
+          a = a'
+      | None =>
+          fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) =>
+          True
+      end
+  | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True
+  end" of type
+ "nth_error Bound (ibound idx) = nth_error Bound (ibound idx) ->
+  e = e -> Prop"
+cannot be applied to the terms
+ "eq_refl" : "nth_error Bound (ibound idx) = nth_error Bound (ibound idx)"
+ "e0" : "nth_error Bound (ibound idx') = e"
+The 2nd term has type "nth_error Bound (ibound idx') = e"
+which should be coercible to "e = e". *)
diff --git a/test-suite/bugs/opened/3346.v b/test-suite/bugs/opened/3346.v
new file mode 100644
index 000000000..8c6856510
--- /dev/null
+++ b/test-suite/bugs/opened/3346.v
@@ -0,0 +1,4 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+Monomorphic Inductive paths (A : Type) (a : A) : A -> Type := idpath : paths A a a.
+(* This should fail with -indices-matter *)
+Check paths nat O O : Prop.
diff --git a/test-suite/bugs/opened/3357.v b/test-suite/bugs/opened/3357.v
new file mode 100644
index 000000000..c47915887
--- /dev/null
+++ b/test-suite/bugs/opened/3357.v
@@ -0,0 +1,9 @@
+Notation D1 := (forall {T : Type} ( x : T ) , Type).
+
+Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1.
+Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33:
+Error: In environment
+A : forall T : Type, T -> Type
+The term "1" has type "nat" while it is expected to have type
+"Type".
+ *)
diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/3363.v
new file mode 100644
index 000000000..800d89573
--- /dev/null
+++ b/test-suite/bugs/opened/3363.v
@@ -0,0 +1,26 @@
+(** In this file, either all four [Check]s should fail, or all four should succeed. *)
+Module A.
+  Section HexStrings.
+    Require Import String.
+  End HexStrings.
+  Fail Check string.
+End A.
+
+Module B.
+  Section HexStrings.
+    Require String.
+    Import String.
+  End HexStrings.
+  Fail Check string.
+End B.
+
+Section HexStrings.
+  Require String.
+  Import String.
+End HexStrings.
+Fail Check string.
+
+Section HexStrings'.
+  Require Import String.
+End HexStrings'.
+Check string.
diff --git a/test-suite/bugs/opened/3368.v b/test-suite/bugs/opened/3368.v
new file mode 100644
index 000000000..c0c00b4ed
--- /dev/null
+++ b/test-suite/bugs/opened/3368.v
@@ -0,0 +1,15 @@
+(* File reduced by coq-bug-finder from 7411 lines to 2271 lines., then from 889 lines to 119 lines, then from 76 lines to 19 lines *)
+Set Universe Polymorphism.
+Set Primitive Projections.
+Record PreCategory := { object :> Type; morphism : object -> object -> Type }.
+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) }.
+Definition opposite (C : PreCategory) : PreCategory := @Build_PreCategory C (fun s d => morphism C d s).
+Fail Definition opposite' C D (F : Functor C D)
+  := Build_Functor (opposite C) (opposite D)
+                   (object_of F)
+                   (fun s d => @morphism_of C D F s d).
+(* Toplevel input, characters 15-191:
+Anomaly: File "pretyping/reductionops.ml", line 149, characters 4-10: Assertion failed.
+Please report. *)
diff --git a/test-suite/bugs/opened/3370.v b/test-suite/bugs/opened/3370.v
new file mode 100644
index 000000000..4964bf96c
--- /dev/null
+++ b/test-suite/bugs/opened/3370.v
@@ -0,0 +1,12 @@
+Require Import String.
+
+Local Ltac set_strings :=
+  let s := match goal with |- context[String ?s1 ?s2] => constr:(String s1 s2) end in
+  let H := fresh s in
+  set (H := s).
+
+Local Open Scope string_scope.
+
+Goal "asdf" = "bds".
+Fail set_strings. (* Error: Ltac variable s is bound to "asdf" which cannot be coerced to
+a fresh identifier. *)
diff --git a/test-suite/bugs/opened/3372.v b/test-suite/bugs/opened/3372.v
new file mode 100644
index 000000000..41ee400fd
--- /dev/null
+++ b/test-suite/bugs/opened/3372.v
@@ -0,0 +1,5 @@
+Set Universe Polymorphism.
+Definition hProp : Type := sigT (fun _ : Type => True).
+Fail Goal hProp@{Set}. (* Toplevel input, characters 15-32:
+Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
+Please report. *)
diff --git a/test-suite/bugs/opened/3373.v b/test-suite/bugs/opened/3373.v
new file mode 100644
index 000000000..8b3b51567
--- /dev/null
+++ b/test-suite/bugs/opened/3373.v
@@ -0,0 +1,15 @@
+(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 332 lines to 21 lines *)
+Set Universe Polymorphism.
+Axiom admit : forall {T}, T.
+Definition UU := Set.
+Definition UU' := Type.
+Definition hSet:= sigT (fun X : UU' => admit) .
+Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type.
+Coercion pr1hSet: hSet >-> Sortclass.
+Axiom binop : UU -> Type.
+Axiom setwithbinop : Type.
+Definition pr1setwithbinop : setwithbinop -> hSet.
+Fail exact ( @projT1 _ ( fun X : hSet@{i j} => binop X ) ).
+(* Toplevel input, characters 15-69:
+Anomaly: apply_coercion_args: mismatch between arguments and coercion.
+Please report. *)
diff --git a/test-suite/bugs/opened/3374.v b/test-suite/bugs/opened/3374.v
new file mode 100644
index 000000000..8a62838f0
--- /dev/null
+++ b/test-suite/bugs/opened/3374.v
@@ -0,0 +1,50 @@
+(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 331 lines to 59 lines *)
+
+Set Universe Polymorphism.
+Axiom admit : forall {T}, T.
+Notation paths := identity .
+Definition UU := Set.
+Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) .
+Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) .
+Definition hProp := sigT (fun X : Type => admit).
+Definition hProptoType := @projT1 _ _ : hProp -> Type .
+Coercion hProptoType: hProp >-> Sortclass.
+Definition UU' := Type.
+Definition hSet:= sigT (fun X : UU' => admit) .
+Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type.
+Coercion pr1hSet: hSet >-> Sortclass.
+Axiom hsubtypes : UU -> Type.
+Definition hrel ( X : UU ) := X -> X -> hProp.
+Axiom hreldirprod : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ), hrel ( dirprod X Y ) .
+Axiom iseqclass : forall { X : UU } ( R : hrel X ) ( A : hsubtypes X ), Type.
+Definition setquot { X : UU } ( R : hrel X ) : Type := sigT (fun A => iseqclass R A).
+Axiom dirprodtosetquot : forall { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ),
+                           setquot ( hreldirprod RX RY ).
+Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y )
+  := forall x x' x0 x0' : X , R x x' ->  R x0 x0' ->  paths ( f x x0 ) ( f x' x0' ) .
+Axiom setquotuniv : forall  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ), Y .
+Definition setquotuniv2  { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R )
+: Y .
+Proof.
+  intros .
+  set ( RR := hreldirprod R R ) .
+  apply (setquotuniv RR Y admit).
+  apply (dirprodtosetquot R R).
+  apply dirprodpair; [ exact c | exact c0 ].
+  Undo.
+  Fail exact (dirprodpair c c0).
+  (* Toplevel input, characters 39-40:
+Error:
+In environment
+X : UU
+R : hrel X
+Y : hSet
+f : X -> X -> Y
+is : iscomprelfun2 R f
+c : setquot R
+c0 : setquot R
+RR := hreldirprod R R : hrel (dirprod X X)
+The term "c" has type "setquot R" while it is expected to have type
+"?42" (unable to find a well-typed instantiation for
+"?42": cannot unify"Type" and "UU").
+ *)
diff --git a/test-suite/bugs/opened/3375.v b/test-suite/bugs/opened/3375.v
new file mode 100644
index 000000000..9cb43413b
--- /dev/null
+++ b/test-suite/bugs/opened/3375.v
@@ -0,0 +1,48 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-impredicative-set") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 330 lines to 45 lines *)
+
+Set Universe Polymorphism.
+Axiom admit : forall {T}, T.
+Definition UU := Set.
+Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) .
+Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) .
+Definition hProp := sigT (fun X : Type => admit).
+Axiom hProppair : forall ( X : UU ) ( is : admit ), hProp@{Set i}.
+Definition hProptoType := @projT1 _ _ : hProp -> Type .
+Coercion hProptoType: hProp >-> Sortclass.
+Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ).
+Definition ishinh ( X : UU ) : hProp := hProppair ( ishinh_UU X ) admit.
+Definition hsubtypes ( X : UU ) : Type := X -> hProp.
+Axiom carrier : forall { X : UU } ( A : hsubtypes X ), Type.
+Definition hrel ( X : UU ) : Type := X -> X -> hProp.
+Set Printing Universes.
+Definition iseqclass { X : UU } ( R : hrel X ) ( A : hsubtypes X ) : Type.
+  intros; exact ( dirprod ( ishinh ( carrier A ) ) ( dirprod ( forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 )
+                                                             ( forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) )) .
+Defined.
+Definition iseqclassconstr' { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) )
+           ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) : iseqclass R A.
+  intros.
+  apply dirprodpair. { exact ax0. }
+                     apply dirprodpair. { exact ax1. } {exact ax2. }
+Defined.
+Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) )
+           ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 ->  A x2 -> R x1 x2 ) : iseqclass R A.
+  pose @iseqclassconstr'.
+  intros.
+  exact (dirprodpair ax0 (dirprodpair ax1 ax2)).
+Fail Defined.
+(* Toplevel input, characters 15-23:
+Error: Illegal application:
+The term "dirprodpair" of type
+ "forall (X Y : UU) (x : X), (fun _ : X => Y) x -> {_ : X & Y}"
+cannot be applied to the terms
+ "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2"
+   : "Type@{max(Set, Top.476, Top.479)}"
+ "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2"
+   : "Type@{max(Set, Top.476, Top.479)}"
+ "ax1" : "forall x1 x2 : X, R x1 x2 -> A x1 -> A x2"
+ "ax2" : "forall x1 x2 : X, A x1 -> A x2 -> R x1 x2"
+The 1st term has type "Type@{max(Set, Top.476, Top.479)}"
+which should be coercible to "UU".
+ *)