More test-suite cases

29 files changed, 1464 insertions, 129 deletions

diff --git a/test-suite/bugs/closed/3260.v b/test-suite/bugs/closed/3260.v
new file mode 100644
index 000000000..9f0231d91
--- /dev/null
+++ b/test-suite/bugs/closed/3260.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+Goal forall m n, n = m -> n+n = m+m.
+intros.
+replace n with m at 2.
+lazymatch goal with
+|- n + m = m + m => idtac
+end.
diff --git a/test-suite/bugs/closed/3264.v b/test-suite/bugs/closed/3264.v
new file mode 100644
index 000000000..4eb218906
--- /dev/null
+++ b/test-suite/bugs/closed/3264.v
@@ -0,0 +1,45 @@
+Module File1.
+  Module Export DirA.
+    Module A.
+      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.
+    End A.
+  End DirA.
+End File1.
+
+Module File2.
+  Module Export DirA.
+    Module B.
+      Import File1.
+      Export A.
+      Lemma foo : forall x y : Type, x = y -> y = x.
+      Proof.
+        intros x y H.
+        rewrite <- H.
+        constructor.
+      Qed.
+    End B.
+  End DirA.
+End File2.
+
+Module File3.
+  Module Export DirA.
+    Module C.
+      Import File1.
+      Export A.
+      Lemma bar : forall x y : Type, x = y -> y = x.
+      Proof.
+        intros x y H.
+        rewrite <- H.
+        constructor.
+      Defined.
+      Definition bar'
+        := Eval cbv beta iota zeta delta [bar internal_paths_rew] in bar.
+    End C.
+  End DirA.
+End File3.
diff --git a/test-suite/bugs/closed/3266.v b/test-suite/bugs/closed/3266.v
new file mode 100644
index 000000000..fd4cbff85
--- /dev/null
+++ b/test-suite/bugs/closed/3266.v
@@ -0,0 +1,3 @@
+Class A := a : nat.
+Lemma p : True.
+Proof. cut A; [tauto | exact 1]. Qed.
diff --git a/test-suite/bugs/closed/328.v b/test-suite/bugs/closed/328.v
new file mode 100644
index 000000000..52cfbbc49
--- /dev/null
+++ b/test-suite/bugs/closed/328.v
@@ -0,0 +1,40 @@
+Module Type TITI.
+Parameter B:Set.
+Parameter x:B.
+Inductive A:Set:=
+a1:B->A.
+Definition f2: A ->B
+:= fun (a:A) =>
+match a with
+ (a1 b)=>b
+end.
+Definition f: A -> B:=fun (a:A) => x.
+End TITI.
+
+
+Module Type TIT.
+Declare Module t:TITI.
+End TIT.
+
+Module Seq(titi:TIT).
+Module t:=titi.t.
+Inductive toto:t.A->t.B->Set:=
+t1:forall (a:t.A), (toto a (t.f a))
+| t2:forall (a:t.A), (toto a (t.f2 a)).
+End Seq.
+
+Module koko(tit:TIT).
+Module seq:=Seq tit.
+Module t':=tit.t.
+
+Definition def:forall (a:t'.A), (seq.toto a (t'.f a)).
+intro ; constructor 1.
+Defined.
+
+Definition def2: forall (a:t'.A), (seq.toto a (t'.f2 a)).
+intro; constructor 2.
+(*  Toplevel input, characters 0-13
+  constructor 2.
+  ^^^^^^^^^^^^^
+Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with
+ (seq.toto a (t'.f2 a)).*)
diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v
new file mode 100644
index 000000000..b08b7ab3c
--- /dev/null
+++ b/test-suite/bugs/closed/3286.v
@@ -0,0 +1,41 @@
+Require Import FunctionalExtensionality.
+
+Ltac make_apply_under_binders_in lem H :=
+  let tac := make_apply_under_binders_in in
+  match type of H with
+    | forall x : ?T, @?P x
+      => let ret := constr:(fun x' : T =>
+                              let Hx := H x' in
+                              $(let ret' := tac lem Hx in
+                                exact ret')$) in
+         match eval cbv zeta in ret with
+           | fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in
+                                      constr:(Some P')
+         end
+    | _ => let ret := constr:($(match goal with
+                                  | _ => (let H' := fresh in
+                                          pose H as H';
+                                          apply lem in H';
+                                          exact (Some H'))
+                                  | _ => exact (@None nat)
+                                end
+                               )$) in
+           let ret' := (eval cbv beta zeta in ret) in
+           constr:(ret')
+    | _ => constr:(@None nat)
+  end.
+
+Ltac apply_under_binders_in lem H :=
+  let H' := make_apply_under_binders_in lem H in
+  let H'0 := match H' with Some ?H'0 => constr:(H'0) end in
+  let H'' := fresh in
+  pose proof H'0 as H'';
+    clear H;
+    rename H'' into H.
+
+Goal forall A B C (f g : forall (x : A) (y : B x), C x y), (forall x y, f x y = g x y) -> True.
+Proof.
+  intros A B C f g H.
+  let lem := constr:(@functional_extensionality_dep) in
+  apply_under_binders_in lem H.
+(* Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/closed/329.v b/test-suite/bugs/closed/329.v
new file mode 100644
index 000000000..def6ed98d
--- /dev/null
+++ b/test-suite/bugs/closed/329.v
@@ -0,0 +1,100 @@
+Module Sylvain_Boulme.
+Module Type Essai.
+Parameter T: Type.
+Parameter my_eq: T -> T -> Prop.
+Parameter my_eq_refl: forall (x:T), (my_eq x x).
+Parameter c: T.
+End Essai.
+
+Module Type Essai2.
+Declare Module M: Essai.
+Parameter c2: M.T.
+End Essai2.
+
+Module Type Essai3.
+Declare Module M: Essai.
+Parameter c3: M.T.
+End Essai3.
+
+Module Type Lift.
+Declare Module Core: Essai.
+Declare Module M: Essai.
+Parameter lift: Core.T -> M.T.
+Parameter lift_prop:forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
+End Lift.
+
+Module I2 (X:Essai) <: Essai2.
+ Module Core := X.
+ Module M<:Essai.
+  Definition T:Type :=Prop.
+  Definition my_eq:=(@eq Prop).
+  Definition c:=True.
+  Lemma my_eq_refl: forall (x:T), (my_eq x x).
+  Proof.
+    unfold my_eq; auto.
+  Qed.
+ End M.
+ Definition c2:=False.
+ Definition lift:=fun (_:Core.T) => M.c.
+ Definition lift_prop: forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c).
+ Proof.
+   unfold lift, M.my_eq; auto.
+ Qed.
+End I2.
+
+Module I4(X:Essai3) (L: Lift with Module Core := X.M) <: Essai3 with Module
+M:=L.M.
+  Module M:=L.M.
+  Definition c3:=(L.lift X.c3).
+End I4.
+
+Module I5(X:Essai3).
+  Module Toto<:  Lift with Module Core := X.M := I2(X.M).
+  Module E4<: Essai3 with Module M:=Toto.M := I4(X)(Toto).
+(*
+Le typage de E4 echoue avec le message
+ Error: Signature components for label my_eq_refl do not match
+ *)
+
+  Module E3<: Essai3 := I4(X)(Toto).
+
+ Definition zarb: forall (x:Toto.M.T), (Toto.M.my_eq x x) := E3.M.my_eq_refl.
+End I5.
+End Sylvain_Boulme.
+
+
+Module Jacek.
+
+    Module Type SIG.
+    End SIG.
+    Module N.
+      Definition A:=Set.
+    End N.
+    Module Type SIG2.
+      Declare Module M:SIG.
+      Parameter B:Type.
+    End SIG2.
+    Module F(X:SIG2 with Module M:=N) (Y:SIG2 with Definition B:=X.M.A).
+    End F.
+End Jacek.
+
+
+Module anoun.
+    Module Type TITI.
+    Parameter X: Set.
+    End TITI.
+
+    Module Type Ex.
+    Declare Module t: TITI.
+    Parameter X : t.X -> t.X -> Set.
+    End Ex.
+
+    Module unionEx(X1: Ex) (X2:Ex with Module t :=X1.t): Ex.
+    Module t:=X1.t.
+    Definition X :=fun (a b:t.X) => ((X1.X a b)+(X2.X a b))%type.
+    End unionEx.
+End anoun.
+(* Le warning qui s'affiche lors de la compilation est le suivant :
+    TODO:replace module after with!
+    Est ce qu'il y'a qq1 qui pourrait m'aider à comprendre le probleme?!
+    Je vous remercie d'avance *)
diff --git a/test-suite/bugs/closed/331.v b/test-suite/bugs/closed/331.v
new file mode 100644
index 000000000..9ef796faf
--- /dev/null
+++ b/test-suite/bugs/closed/331.v
@@ -0,0 +1,20 @@
+Module Type TIT.
+
+Inductive X:Set:=
+ b:X.
+End TIT.
+
+
+Module Type TOTO.
+Declare Module t:TIT.
+Inductive titi:Set:=
+ a:t.X->titi.
+End TOTO.
+
+
+Module toto (ta:TOTO).
+Module ti:=ta.t.
+
+Definition ex1:forall (c d:ti.X), (ta.a d)=(ta.a c) -> d=c.
+intros.
+injection H.
diff --git a/test-suite/bugs/closed/3332.v b/test-suite/bugs/closed/3332.v
new file mode 100644
index 000000000..d86470cde
--- /dev/null
+++ b/test-suite/bugs/closed/3332.v
@@ -0,0 +1,6 @@
+(* -*- 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/closed/3350.v b/test-suite/bugs/closed/3350.v
new file mode 100644
index 000000000..bab197ed0
--- /dev/null
+++ b/test-suite/bugs/closed/3350.v
@@ -0,0 +1,115 @@
+Require Coq.Vectors.Fin.
+Require Coq.Vectors.Vector.
+
+Local Generalizable All Variables.
+Set Implicit Arguments.
+
+Arguments Fin.F1 : clear implicits.
+
+Lemma fin_0_absurd : notT (Fin.t 0).
+Proof. hnf. apply Fin.case0. Qed.
+
+Fixpoint lower {n:nat} (p:Fin.t (S n)) {struct p} :
+  forall (i:Fin.t (S n)), option (Fin.t n)
+  := match p in Fin.t (S n1)
+           return Fin.t (S n1) -> option (Fin.t n1)
+     with
+       | @Fin.F1 n1 =>
+         fun (i:Fin.t (S n1)) =>
+           match i in Fin.t (S n2) return option (Fin.t n2) with
+             | @Fin.F1 n2 => None
+             | @Fin.FS n2 i2 => Some i2
+           end
+       | @Fin.FS n1 p1 =>
+         fun (i:Fin.t (S n1)) =>
+           match i in Fin.t (S n2) return Fin.t n2 -> option (Fin.t n2) with
+             | @Fin.F1 n2 =>
+               match n2 as n3 return Fin.t n3 -> option (Fin.t n3) with
+                 | 0 => fun p2 => False_rect _ (fin_0_absurd p2)
+                 | S n3 => fun p2 => Some (Fin.F1 n3)
+               end
+             | @Fin.FS n2 i2 =>
+               match n2 as n3 return Fin.t n3 -> Fin.t n3 -> option (Fin.t n3) with
+                 | 0 => fun i3 p3 => False_rect _ (fin_0_absurd p3)
+                 | S n3 => fun (i3 p3:Fin.t (S n3)) =>
+                             option_map (@Fin.FS _) (lower p3 i3)
+               end i2
+           end p1
+     end.
+
+Lemma lower_ind (P: forall n (p i:Fin.t (S n)), option (Fin.t n) -> Prop)
+      (c11 : forall n, P n (Fin.F1 n) (Fin.F1 n) None)
+      (c1S : forall n (i:Fin.t n), P n (Fin.F1 n) (Fin.FS i) (Some i))
+      (cS1 : forall n (p:Fin.t (S n)),
+               P (S n) (Fin.FS p) (Fin.F1 (S n)) (Some (Fin.F1 n)))
+      (cSSS : forall n (p i:Fin.t (S n)) (i':Fin.t n)
+                     (Elow:lower p i = Some i'),
+                P n p i (Some i') ->
+                P (S n) (Fin.FS p) (Fin.FS i) (Some (Fin.FS i')))
+      (cSSN : forall n (p i:Fin.t (S n))
+                (Elow:lower p i = None),
+                P n p i None ->
+                P (S n) (Fin.FS p) (Fin.FS i) None) :
+  forall n (p i:Fin.t (S n)), P n p i (lower p i).
+Proof.
+  fix 2. intros n p.
+  refine (match p as p1 in Fin.t (S n1)
+                return forall (i1:Fin.t (S n1)), P n1 p1 i1 (lower p1 i1)
+          with
+            | @Fin.F1 n1 => _
+            | @Fin.FS n1 p1 => _
+          end); clear n p.
+  { revert n1. refine (@Fin.caseS _ _ _); cbn; intros.
+    apply c11. apply c1S. }
+  { intros i1. revert p1.
+    pattern n1, i1; refine (@Fin.caseS _ _ _ _ _);
+    clear n1 i1;
+    (intros [|n] i; [refine (False_rect _ (fin_0_absurd i)) | cbn ]).
+    { apply cS1. }
+    { intros p. pose proof (lower_ind n p i) as H.
+      destruct (lower p i) eqn:E.
+      { apply cSSS; assumption. }
+      { cbn. apply cSSN; assumption. } } }
+Qed.
+
+Section squeeze.
+  Context {A:Type} (x:A).
+  Notation vec := (Vector.t A).
+
+  Fixpoint squeeze {n} (v:vec n) (i:Fin.t (S n)) {struct i} : vec (S n) :=
+    match i in Fin.t (S _n) return vec _n -> vec (S _n)
+    with
+      | @Fin.F1 n' => fun v' => Vector.cons _ x _ v'
+      | @Fin.FS n' i' =>
+        fun v' =>
+          match n' as _n return vec _n -> Fin.t _n -> vec (S _n)
+          with
+            | 0 => fun u i' => False_rect _ (fin_0_absurd i')
+            | S m =>
+              fun (u:vec (S m)) =>
+                match u in Vector.t _ (S _m)
+                      return Fin.t (S _m) -> vec (S (S _m))
+                with
+                  | Vector.nil _ => tt
+                  | Vector.cons _ h _ u' =>
+                    fun j' => Vector.cons _ h _ (squeeze u' j')
+                end
+          end v' i'
+    end v.
+End squeeze.
+
+Lemma squeeze_nth (A:Type) (x:A) (n:nat) (v:Vector.t A n) p i :
+  Vector.nth (squeeze x v p) i = match lower p i with
+                                   | Some j => Vector.nth v j
+                                   | None => x
+                                 end.
+Proof.
+  (* alternatively: [functional induction (lower p i) using lower_ind] *)
+  revert v. pattern n, p, i, (lower p i).
+  refine (@lower_ind _ _ _ _ _ _ n p i);
+    intros; cbn; auto.
+
+  (*** Fails here with "Conversion test raised an anomaly" ***)
+  revert v.
+
+Abort.
diff --git a/test-suite/bugs/closed/3372.v b/test-suite/bugs/closed/3372.v
new file mode 100644
index 000000000..91e3df76d
--- /dev/null
+++ b/test-suite/bugs/closed/3372.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Definition hProp : Type := sigT (fun _ : Type => True).
+Goal Type.
+Fail exact hProp@{Set}. (* test that it fails, but is not an anomaly *)
+try (exact hProp@{Set}; fail 1). (* Toplevel input, characters 15-32:
+Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
+Please report. *)
diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v
index 16b137091..5ecf28015 100644
--- a/test-suite/bugs/closed/3373.v
+++ b/test-suite/bugs/closed/3373.v
@@ -5,15 +5,29 @@ 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.
-Goal True.
-pose (( @projT1 _ ( fun X : hSet@{Set j k} => binop X ) ) : _ -> hSet).
-Admitted.
\ No newline at end of file
+Module short.
+  Record foo := { bar : Type }.
+  Coercion baz (x : foo@{Set}) : Set := bar x.
+  Goal True.
+  Proof.
+    Fail pose ({| bar := Set |} : Type). (* check that it fails *)
+    try pose ({| bar := Set |} : Type). (* Anomaly: apply_coercion_args: mismatch between arguments and coercion.
+Please report. *)
+  Admitted.
+End short.
+
+Module long.
+  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.
+  Goal True.
+  Proof.
+    Fail pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it fails *)
+    try pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it's not an anomaly *)
+  Admitted.
+End long.
diff --git a/test-suite/bugs/closed/3382.v b/test-suite/bugs/closed/3382.v
new file mode 100644
index 000000000..1d8e91674
--- /dev/null
+++ b/test-suite/bugs/closed/3382.v
@@ -0,0 +1,63 @@
+(* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines, then from 139 lines to 114 lines, then from 93 lines to 77 lines *)
+
+Set Implicit Arguments.
+Definition admit {T} : T.
+Admitted.
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+Reserved Infix "o" (at level 40, left associativity).
+Record PreCategory :=
+  { Object :> Type;
+    Morphism : Object -> Object -> Type;
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g) }.
+Bind Scope category_scope with PreCategory.
+Infix "o" := (@Compose _ _ _ _) : morphism_scope.
+Local Open Scope morphism_scope.
+Record Functor (C D : PreCategory) :=
+  { ObjectOf :> C -> D;
+    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
+    FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
+                       MorphismOf _ _ (m2 o m1) = (MorphismOf _ _ m2) o (MorphismOf _ _ m1) }.
+Bind Scope functor_scope with Functor.
+Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+Definition ComposeFunctors C D E
+           (G : Functor D E) (F : Functor C D) : Functor C E
+  := Build_Functor C E (fun c => G (F c)) admit admit.
+Infix "o" := ComposeFunctors : functor_scope.
+Record NaturalTransformation C D (F G : Functor C D) :=
+  { ComponentsOf :> forall c, D.(Morphism) (F c) (G c);
+    Commutes : forall s d (m : C.(Morphism) s d),
+                 ComponentsOf d o F.(MorphismOf) m = G.(MorphismOf) m o ComponentsOf s }.
+Definition NTComposeT C D (F F' F'' : Functor C D)
+           (T' : NaturalTransformation F' F'')
+           (T : NaturalTransformation F F')
+           (CO := fun c => T' c o T c)
+: NaturalTransformation F F''.
+  exact (Build_NaturalTransformation F F''
+                                     (fun c => T' c o T c)
+                                     (admit : forall s d (m : Morphism C s d), CO d o MorphismOf F m = MorphismOf F'' m o CO s)).
+Defined.
+Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F')
+           (G : Functor C D)
+  := Build_NaturalTransformation (F o G) (F' o G) (fun c => T (G c)) admit.
+Axiom NTWhiskerR_CompositionOf
+: forall C D
+         (F G H : Functor C D)
+         (T : NaturalTransformation G H)
+         (T' : NaturalTransformation F G) B (I : Functor B C),
+    NTComposeT (NTWhiskerR T I) (NTWhiskerR T' I) = NTWhiskerR (NTComposeT T T') I.
+Definition FunctorCategory C D : PreCategory
+  := @Build_PreCategory (Functor C D)
+                        (NaturalTransformation (C := C) (D := D))
+                        admit.
+Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
+Class silly {T} := term : T.
+Timeout 1 Fail Definition NTWhiskerR_Functorial (C D E : PreCategory) (G : [C, D]%category)
+: [[D, E], [C, E]]%category
+  := Build_Functor
+       [C, D] [C, E]
+       (fun F => _ : silly)
+       (fun _ _ T => _ : silly)
+       (fun _ _ _ _ _ => NTWhiskerR_CompositionOf _ _ _).
diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v
new file mode 100644
index 000000000..0e236c217
--- /dev/null
+++ b/test-suite/bugs/closed/3386.v
@@ -0,0 +1,16 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Record Cat := { Obj :> Type }.
+Definition set_cat := {| Obj := Type |}.
+Goal Type@{i} = Type@{j}.
+Proof.
+  (* 1 subgoals
+, subgoal 1 (ID 3)
+
+  ============================
+   Type@{Top.368} = Type@{Top.370}
+(dependent evars:) *)
+  Fail change Type@{i} with (Obj set_cat@{i}). (* check that it fails *)
+  try change Type@{i} with (Obj set_cat@{i}). (* check that it's not an anomaly *)
+(* Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
+Please report. *)
diff --git a/test-suite/bugs/closed/3390.v b/test-suite/bugs/closed/3390.v
new file mode 100644
index 000000000..eb3c4f4b9
--- /dev/null
+++ b/test-suite/bugs/closed/3390.v
@@ -0,0 +1,9 @@
+Tactic Notation "basicapply" open_constr(R) "using" tactic3(tac) "sideconditions" tactic0(tacfin) := idtac.
+Tactic Notation "basicapply" open_constr(R) := basicapply R using (fun Hlem => idtac) sideconditions (autounfold with spred; idtac).
+(* segfault in coqtop *)
+
+
+Tactic Notation "basicapply" tactic0(tacfin) := idtac.
+
+Goal True.
+basicapply subst.
diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v
new file mode 100644
index 000000000..ec25e6829
--- /dev/null
+++ b/test-suite/bugs/closed/3393.v
@@ -0,0 +1,152 @@
+(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *)
+Set Universe Polymorphism.
+Axiom admit : forall {T}, T.
+Set Implicit Arguments.
+Generalizable All Variables.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "a = b" := (@paths _ a b) : type_scope.
+Arguments idpath {A a} , [A] a.
+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 }.
+Delimit Scope equiv_scope with equiv.
+Local Open Scope equiv_scope.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+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) : (forall x, f x = g x) -> f = g := (@apD10 A P f g)^-1.
+Record PreCategory :=
+  { object :> Type;
+    morphism : object -> object -> Type;
+    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)
+  }.
+Bind Scope category_scope with PreCategory.
+Bind Scope morphism_scope with morphism.
+Infix "o" := (@compose _ _ _ _) : morphism_scope.
+Delimit Scope functor_scope with functor.
+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) }.
+Bind Scope functor_scope with Functor.
+Notation "F '_1' m" := (@morphism_of _ _ F _ _ m) (at level 10, no associativity) : morphism_scope.
+Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
+Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope.
+Class Isomorphic {C : PreCategory} s d :=
+  { morphism_isomorphic :> morphism C s d;
+    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Coercion morphism_isomorphic : Isomorphic >-> morphism.
+Definition isisomorphism_inverse `(@IsIsomorphism C x y m) : IsIsomorphism m^-1 := {| morphism_inverse := m |}.
+
+Global Instance isisomorphism_compose `(@IsIsomorphism C y z m0) `(@IsIsomorphism C x y m1) : IsIsomorphism (m0 o m1).
+Admitted.
+Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
+Definition composef C D E (G : Functor D E) (F : Functor C D) : Functor C E
+  := Build_Functor
+       C E
+       (fun c => G (F c))
+       (fun _ _ m => @morphism_of _ _ G _ _ (@morphism_of _ _ F _ _ m)).
+Infix "o" := composef : functor_scope.
+Delimit Scope natural_transformation_scope with natural_transformation.
+
+Local Open Scope morphism_scope.
+Record NaturalTransformation C D (F G : Functor C D) :=
+  { 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 }.
+
+Definition composet C D (F F' F'' : Functor C D) (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F')
+: NaturalTransformation F F''
+  := Build_NaturalTransformation F F'' (fun c => T' c o T c) admit.
+Infix "o" := composet : natural_transformation_scope.
+Section path_natural_transformation.
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variables F G : Functor C D.
+  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
+    : (forall x, components_of T x = components_of U x)
+      -> 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.
+
+Local Open Scope natural_transformation_scope.
+Definition associativityt `{fs : Funext}
+           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.
+Definition functor_category `{Funext} (C D : PreCategory) : PreCategory
+  := @Build_PreCategory (Functor C D) (@NaturalTransformation C D) (@composet C D) (@associativityt _ C D).
+Notation "C -> D" := (functor_category C D) : category_scope.
+Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G := @Isomorphic (C -> D) F G.
+Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope.
+Global Instance isisomorphism_compose' `{Funext}
+       `(T' : @NaturalTransformation C D F' F'')
+       `(T : @NaturalTransformation C D F F')
+       `{@IsIsomorphism (C -> D) F' F'' T'}
+       `{@IsIsomorphism (C -> D) F F' T}
+: @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
+  := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.
+Section lemmas.
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Variable F : C -> PreCategory.
+  Context
+    {w y z}
+    {f : Functor (F w) (F z)} {f0 : Functor (F w) (F y)}
+    {f2 : Functor (F y) (F z)}
+    {f5 : Functor (F w) (F z)}
+    {n2 : f <~=~> (f2 o f0)%functor}.
+  Lemma p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper' XX
+  : @IsIsomorphism
+      (F w -> F z) f5 f
+      (n2 ^-1 o XX)%natural_transformation.
+  Proof.
+    eapply isisomorphism_compose'.
+    eapply isisomorphism_inverse. (* Toplevel input, characters 22-43:
+Error:
+In environment
+H : Funext
+C : PreCategory
+F : C -> PreCategory
+w : C
+y : C
+z : C
+f : Functor (F w) (F z)
+f0 : Functor (F w) (F y)
+f2 : Functor (F y) (F z)
+f5 : Functor (F w) (F z)
+n2 : f <~=~> (f2 o f0)%functor
+XX : NaturalTransformation f5 (f2 o f0)
+Unable to unify
+ "{|
+  object := Functor (F w) (F z);
+  morphism := NaturalTransformation (D:=F z);
+  compose := composet (D:=F z);
+  associativity := associativityt (D:=F z) |}" with
+ "{|
+  object := Functor (F w) (F z);
+  morphism := NaturalTransformation (D:=F z);
+  compose := composet (D:=F z);
+  associativity := associativityt (D:=F z) |}". *)
diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v
new file mode 100644
index 000000000..6de13f74e
--- /dev/null
+++ b/test-suite/bugs/opened/3263.v
@@ -0,0 +1,231 @@
+(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines,  2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
+Generalizable All Variables.
+Set Implicit Arguments.
+
+Arguments fst {_ _} _.
+Arguments snd {_ _} _.
+
+Axiom cheat : forall {T}, T.
+
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (paths x y) : type_scope.
+
+Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory (object : Type) :=
+  Build_PreCategory' {
+      object :> Type := object;
+      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
+    }.
+Bind Scope category_scope with PreCategory.
+Arguments PreCategory {_}.
+Arguments identity {_} [!C%category] x%object : rename.
+
+Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+Infix "o" := compose : morphism_scope.
+
+Delimit Scope functor_scope with functor.
+Local Open Scope morphism_scope.
+Record Functor `(C : @PreCategory objC, D : @PreCategory objD) :=
+  {
+    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)
+  }.
+Bind Scope functor_scope with Functor.
+
+Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+
+Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
+
+Class IsIsomorphism `{C : @PreCategory objC} {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 _
+  }.
+
+Definition opposite `(C : @PreCategory objC) : 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).
+
+Notation "C ^op" := (opposite C) (at level 3) : category_scope.
+
+Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD).
+  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.
+Infix "*" := prod : category_scope.
+
+Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E
+  := Build_Functor
+       C E
+       (fun c => G (F c))
+       (fun _ _ m => morphism_of G (morphism_of F m))
+       cheat
+       cheat.
+
+Infix "o" := compose_functor : functor_scope.
+
+Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) :=
+  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
+    }.
+Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory
+  := @Build_PreCategory' (Functor C D)
+                         (@NaturalTransformation _ C _ D)
+                         cheat
+                         cheat
+                         cheat
+                         cheat
+                         cheat
+                         cheat
+                         cheat.
+
+Definition opposite_functor `(F : @Functor objC C objD 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).
+
+Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op
+  := Build_Functor C (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).
+Notation "F ^op" := (opposite_functor F) : functor_scope.
+
+Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope.
+Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C
+  := Build_Functor (C * D) C
+                   (@fst _ _)
+                   (fun _ _ => @fst _ _)
+                   (fun _ _ _ _ _ => idpath)
+                   (fun _ => idpath).
+
+Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D
+  := Build_Functor (C * D) D
+                   (@snd _ _)
+                   (fun _ _ => @snd _ _)
+                   (fun _ _ _ _ _ => idpath)
+                   (fun _ => idpath).
+Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' 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))%morphism
+       cheat
+       cheat.
+Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D')
+  := (prod_functor (F o fst) (F' o snd))%functor.
+Notation cat_of obj :=
+  (@Build_PreCategory' obj
+                       (fun x y => forall _ : x, y)
+                       (fun _ x => x)
+                       (fun _ _ _ f g x => f (g x))%core
+                       (fun _ _ _ _ _ _ _ => idpath)
+                       (fun _ _ _ _ _ _ _ => idpath)
+                       (fun _ _ _ => idpath)
+                       (fun _ _ _ => idpath)
+                       (fun _ => idpath)).
+
+Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type)
+  := Build_Functor _ _ cheat cheat cheat cheat.
+
+Definition induced_hom_natural_transformation `(F : @Functor objC C objD D)
+: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F)
+  := Build_NaturalTransformation' _ _ cheat cheat cheat.
+
+Class IsFullyFaithful `(F : @Functor objC C objD D)
+  := is_fully_faithful
+     : forall x y : C,
+         IsIsomorphism (induced_hom_natural_transformation F (x, y)).
+
+Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type))
+  := cheat.
+
+Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type))
+  := (((coyoneda A^op)^op'L)^op'L)%functor.
+Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A).
+Admitted.
+
+Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A).
+Proof.
+  intros a b.
+  pose proof (coyoneda_embedding A^op a b) as CYE.
+  unfold yoneda.
+  Time let t := (type of CYE) in
+  let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *)
+  Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in
+  let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE').
+  Time let t := match goal with |- ?G => constr:(G) end in
+  let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *)
+Fail Timeout 2 Defined.
+Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *)
+
+Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A).
+Proof.
+  intros a b.
+  pose proof (coyoneda_embedding A^op a b) as CYE.
+  unfold yoneda; simpl in *.
+  Fail Timeout 1 exact CYE.
+  Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *)
+Fail Timeout 60 Defined. (* Timeout! *)
diff --git a/test-suite/bugs/opened/3267.v b/test-suite/bugs/opened/3267.v
new file mode 100644
index 000000000..43eb1377d
--- /dev/null
+++ b/test-suite/bugs/opened/3267.v
@@ -0,0 +1,37 @@
+Module a.
+  Hint Extern 0 => progress subst.
+  Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y.
+  Proof.
+    intros.
+    (* this should not fail *)
+    Fail progress eauto.
+    admit.
+  Defined.
+End a.
+
+Module b.
+  Hint Extern 0 => progress subst.
+  Goal forall T (x y : T) (P Q : _ -> Prop), y = x -> (P x -> Q x) -> P y -> Q y.
+  Proof.
+    intros.
+    eauto.
+  Defined.
+End b.
+
+Module c.
+  Hint Extern 0 => progress subst; eauto.
+  Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y.
+  Proof.
+    intros.
+    eauto.
+  Defined.
+End c.
+
+Module d.
+  Hint Extern 0 => progress subst; repeat match goal with H : _ |- _ => revert H end.
+  Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y.
+  Proof.
+    intros.
+    eauto.
+  Defined.
+End d.
diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v
new file mode 100644
index 000000000..19ed787d1
--- /dev/null
+++ b/test-suite/bugs/opened/3277.v
@@ -0,0 +1,7 @@
+Tactic Notation "evarr" open_constr(x) := let y := constr:(x) in exact y.
+
+Goal True.
+  evarr _.
+Admitted.
+Goal True.
+  Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *)
diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v
new file mode 100644
index 000000000..2c6d391a0
--- /dev/null
+++ b/test-suite/bugs/opened/3278.v
@@ -0,0 +1,25 @@
+Module a.
+  Fail Check let x' := _ in
+             $(exact x')$.
+
+  Notation foo x := (let x' := x in $(exact x')$).
+
+  Fail Check foo _. (* Error:
+Cannot infer an internal placeholder of type "Type" in environment:
+
+x' := ?42 : ?41
+. *)
+End a.
+
+Module b.
+  Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I).
+  Notation bar x := (let x' := x in let y := (I : True) in I).
+
+  Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *)
+  Check bar _. (* let x' := ?9 in let y := I in I *)
+  Fail Check foo _. (* Error:
+Cannot infer an internal placeholder of type "Type" in environment:
+
+x' := ?42 : ?41
+. *)
+End b.
diff --git a/test-suite/bugs/opened/3300.v b/test-suite/bugs/opened/3300.v
new file mode 100644
index 000000000..955cfc3aa
--- /dev/null
+++ b/test-suite/bugs/opened/3300.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/3301.v b/test-suite/bugs/opened/3301.v
index 955cfc3aa..dbcb7f067 100644
--- a/test-suite/bugs/opened/3301.v
+++ b/test-suite/bugs/opened/3301.v
@@ -1,120 +1,10 @@
-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.
+Require Import Coq.Init.Specif Coq.Init.Datatypes Coq.Init.Logic.
 
-Theorem pandora : False.
-apply (paradox down up back forth backforth backforth_r).
-Qed.
+Parameters A B : Prop.
+Parameter P : A -> Prop.
 
-Print Assumptions pandora.
-(* Closed under the global context *)
+Fail Check fun x : sigT P => (eq_refl : x = existT P (projT1 x) (projT2 x)).
+Fail Check fun x : sig P => (eq_refl : x = exist P (proj1_sig x) (proj2_sig x)).
+Fail Check fun x : A * B => (eq_refl : x = (fst x, snd x)).
+Fail Check fun x : A /\ B => (eq_refl : x = conj (proj1 x) (proj2 x)).
diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v
new file mode 100644
index 000000000..529cc737d
--- /dev/null
+++ b/test-suite/bugs/opened/3304.v
@@ -0,0 +1,3 @@
+Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$.
+(* The command has indeed failed with message:
+=> Error: Special token .. is for use in the Notation command. *)
diff --git a/test-suite/bugs/opened/3377.v b/test-suite/bugs/opened/3377.v
new file mode 100644
index 000000000..9ad3779d1
--- /dev/null
+++ b/test-suite/bugs/opened/3377.v
@@ -0,0 +1,8 @@
+Set Primitive Projections.
+Record prod A B := pair { fst : A; snd : B}.
+
+Goal fst (@pair Type Type Type Type).
+Set Printing All.
+Fail match goal with |- ?f _ => idtac end.
+(* Toplevel input, characters 7-44:
+Error: No matching clauses for match. *)
diff --git a/test-suite/bugs/opened/3383.v b/test-suite/bugs/opened/3383.v
new file mode 100644
index 000000000..9a14641a5
--- /dev/null
+++ b/test-suite/bugs/opened/3383.v
@@ -0,0 +1,7 @@
+Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end.
+intro.
+Fail lazymatch goal with
+| [ |- appcontext[match ?b as b' return @?P b' with true => ?t | false => ?f end] ]
+  => change (match b as b' return P b with true => t | false => f end) with (@bool_rect P t f)
+end. (* Toplevel input, characters 153-154:
+Error: The reference P was not found in the current environment. *)
diff --git a/test-suite/bugs/opened/3385.v b/test-suite/bugs/opened/3385.v
new file mode 100644
index 000000000..b4da9cf67
--- /dev/null
+++ b/test-suite/bugs/opened/3385.v
@@ -0,0 +1,22 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category := { ob : Type }.
+
+Goal forall C, ob C -> ob C.
+intros C X.
+
+let y := (eval compute in (ob C)) in constr_eq y (ob C). (* success *)
+let y := (eval compute in (@ob C)) in constr_eq y (ob C). (* success *)
+(* should be [Fail let y := (eval compute in (@ob C)) in constr_eq y (@ob C).] (really [let y := (eval compute in (@ob C)) in constr_eq y (@ob C)] should succeed, but so long as the [Fail] succeeds, this bug is open), but "not equal" escapes [Fail]. *)
+try (let y := (eval compute in (@ob C)) in constr_eq y (@ob C); fail 1). (* failure *)
+try (constr_eq (@ob C) (ob C); fail 1). (* failure *)
+let y := constr:(@ob C) in
+match y with
+  | ?f C => idtac
+end. (* success *)
+try (let y := constr:(@ob C) in
+match eval compute in y with
+  | ?f C => idtac
+end; fail 1). (* failure: no matching clauses for match *)
diff --git a/test-suite/bugs/opened/3387.v b/test-suite/bugs/opened/3387.v
new file mode 100644
index 000000000..16c4e7da2
--- /dev/null
+++ b/test-suite/bugs/opened/3387.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Record Cat := { Obj :> Type }.
+Definition set_cat := {| Obj := Type |}.
+Goal Type@{i} = Type@{j}.
+Proof.
+  (* 1 subgoals
+, subgoal 1 (ID 3)
+
+  ============================
+   Type@{Top.368} = Type@{Top.370}
+(dependent evars:) *)
+  let x := constr:(Type) in
+  let y := constr:(Obj set_cat) in
+  unify x y. (* success *)
+  Fail let x := constr:(Type) in
+  let y := constr:(Obj set_cat) in
+  first [ unify x y | fail 2 "no unify" ];
+    change x with y. (* Error: Not convertible. *)
diff --git a/test-suite/bugs/opened/3388.v b/test-suite/bugs/opened/3388.v
new file mode 100644
index 000000000..d0ea72e1f
--- /dev/null
+++ b/test-suite/bugs/opened/3388.v
@@ -0,0 +1,57 @@
+Inductive test : bool -> bool -> Type :=
+| test00 : test false false
+| test01 : test false true
+| test10 : test true false
+.
+
+(* This does not work *)
+Fail Definition test_a (t : test true false) : test true false :=
+  match t with
+    | test10 => test10
+  end.
+
+(* The following definition shows that test_a SHOULD work *)
+Definition test_a_workaround (t : test true false) : test true false :=
+  match t with
+    | test10 => test10
+    | _ => tt
+  end.
+
+(* Surprisingly, this works *)
+Definition test_b (t : test false true) : test false true :=
+  match t with
+    | test01 => test01
+  end.
+
+
+(* This, too, works *)
+Definition test_c x (t : test false x) : test false x :=
+  match t with
+    | test00 => test00
+    | test01 => test01
+  end.
+
+Inductive test2 : bool -> bool -> Type :=
+| test201 : test2 false true
+| test210 : test2 true false
+| test211 : test2 true true
+.
+
+(* Now this works *)
+Definition test2_a (t : test2 true false) : test2 true false :=
+  match t with
+    | test210 => test210
+  end.
+
+(* Accordingly, this now fails *)
+Fail Definition test2_b (t : test2 false true) : test2 false true :=
+  match t with
+    | test201 => test201
+  end.
+
+
+(* This, too, fails *)
+Fail Definition test2_c x (t : test2 false x) : test2 false x :=
+  match t with
+    | test201 => test201
+  end.
diff --git a/test-suite/bugs/opened/3392.v b/test-suite/bugs/opened/3392.v
new file mode 100644
index 000000000..b28943e07
--- /dev/null
+++ b/test-suite/bugs/opened/3392.v
@@ -0,0 +1,41 @@
+(* File reduced by coq-bug-finder from original input, then from 12105 lines to 142 lines, then from 83 lines to 57 lines *)
+Generalizable All Variables.
+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.
+Arguments idpath {A a} , [A] a.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+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 apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): transport _ p (f x) = f y := admit.
+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) }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3).
+Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x), (forall x, f x = g x) -> f = g.
+Axiom isequiv_adjointify : forall {A B} (f : A -> B) (g : B -> A) (isretr : Sect g f) (issect : Sect f g), IsEquiv f.
+Definition functor_forall `{P : A -> Type} `{Q : B -> Type} (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
+: (forall a:A, P a) -> (forall b:B, Q b) := (fun g b => f1 _ (g (f0 b))).
+Goal forall `{P : A -> Type} `{Q : B -> Type} `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)},
+       IsEquiv (functor_forall f g).
+Proof.
+  intros.
+  refine (isequiv_adjointify (functor_forall f g)
+                             (functor_forall (f^-1)
+                                             (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y
+                             )) _ _);
+  intros h.
+  - abstract (
+        apply path_forall; intros b; unfold functor_forall;
+        rewrite eisadj;
+        admit
+      ).
+  - abstract (
+        apply path_forall; intros a; unfold functor_forall;
+        rewrite eissect;
+        apply apD
+      ).
+Fail Defined.
+(* Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/3395.v
new file mode 100644
index 000000000..ff0dbf974
--- /dev/null
+++ b/test-suite/bugs/opened/3395.v
@@ -0,0 +1,230 @@
+(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines,  2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
+Generalizable All Variables.
+Set Implicit Arguments.
+
+Arguments fst {_ _} _.
+Arguments snd {_ _} _.
+
+Axiom cheat : forall {T}, T.
+
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (paths x y) : type_scope.
+
+Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory (object : Type) :=
+  Build_PreCategory' {
+      object :> Type := object;
+      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
+    }.
+Bind Scope category_scope with PreCategory.
+Arguments PreCategory {_}.
+Arguments identity {_} [!C%category] x%object : rename.
+
+Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+Infix "o" := compose : morphism_scope.
+
+Delimit Scope functor_scope with functor.
+Local Open Scope morphism_scope.
+Record Functor `(C : @PreCategory objC, D : @PreCategory objD) :=
+  {
+    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)
+  }.
+Bind Scope functor_scope with Functor.
+
+Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+
+Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope.
+
+Class IsIsomorphism `{C : @PreCategory objC} {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 _
+  }.
+
+Definition opposite `(C : @PreCategory objC) : 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).
+
+Notation "C ^op" := (opposite C) (at level 3) : category_scope.
+
+Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD).
+  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.
+Infix "*" := prod : category_scope.
+
+Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E
+  := Build_Functor
+       C E
+       (fun c => G (F c))
+       (fun _ _ m => morphism_of G (morphism_of F m))
+       cheat
+       cheat.
+
+Infix "o" := compose_functor : functor_scope.
+
+Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) :=
+  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
+    }.
+Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory
+  := @Build_PreCategory' (Functor C D)
+                         (@NaturalTransformation _ C _ D)
+                         cheat
+                         cheat
+                         cheat
+                         cheat
+                         cheat
+                         cheat
+                         cheat.
+
+Definition opposite_functor `(F : @Functor objC C objD 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).
+
+Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op
+  := Build_Functor C (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).
+Notation "F ^op" := (opposite_functor F) : functor_scope.
+
+Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope.
+Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C
+  := Build_Functor (C * D) C
+                   (@fst _ _)
+                   (fun _ _ => @fst _ _)
+                   (fun _ _ _ _ _ => idpath)
+                   (fun _ => idpath).
+
+Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D
+  := Build_Functor (C * D) D
+                   (@snd _ _)
+                   (fun _ _ => @snd _ _)
+                   (fun _ _ _ _ _ => idpath)
+                   (fun _ => idpath).
+Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' 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))%morphism
+       cheat
+       cheat.
+Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D')
+  := (prod_functor (F o fst) (F' o snd))%functor.
+Notation cat_of obj :=
+  (@Build_PreCategory' obj
+                       (fun x y => forall _ : x, y)
+                       (fun _ x => x)
+                       (fun _ _ _ f g x => f (g x))%core
+                       (fun _ _ _ _ _ _ _ => idpath)
+                       (fun _ _ _ _ _ _ _ => idpath)
+                       (fun _ _ _ => idpath)
+                       (fun _ _ _ => idpath)
+                       (fun _ => idpath)).
+
+Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type)
+  := Build_Functor _ _ cheat cheat cheat cheat.
+
+Definition induced_hom_natural_transformation `(F : @Functor objC C objD D)
+: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F)
+  := Build_NaturalTransformation' _ _ cheat cheat cheat.
+
+Class IsFullyFaithful `(F : @Functor objC C objD D)
+  := is_fully_faithful
+     : forall x y : C,
+         IsIsomorphism (induced_hom_natural_transformation F (x, y)).
+
+Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type))
+  := cheat.
+
+Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type))
+  := (((coyoneda A^op)^op'L)^op'L)%functor.
+Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A).
+Admitted.
+
+Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A).
+Proof.
+  intros a b.
+  pose proof (coyoneda_embedding A^op a b) as CYE.
+  unfold yoneda.
+  Time let t := (type of CYE) in
+  let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *)
+  Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in
+  let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE').
+  Time let t := match goal with |- ?G => constr:(G) end in
+  let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *)
+Fail Timeout 2 Defined.
+Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *)
+
+Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A).
+Proof.
+  intros a b.
+  pose proof (coyoneda_embedding A^op a b) as CYE.
+  unfold yoneda; simpl in *.
+  Fail Timeout 1 exact CYE.
+  Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *)