More test-suite cases

14 files changed, 814 insertions, 117 deletions

diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v
new file mode 100644
index 0000000000..6de13f74e3
--- /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 0000000000..43eb1377d2
--- /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 0000000000..19ed787d1e
--- /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 0000000000..2c6d391a0c
--- /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 0000000000..955cfc3aa0
--- /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 955cfc3aa0..dbcb7f0679 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 0000000000..529cc737df
--- /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 0000000000..9ad3779d16
--- /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 0000000000..9a14641a57
--- /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 0000000000..b4da9cf675
--- /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 0000000000..16c4e7da2f
--- /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 0000000000..d0ea72e1fd
--- /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 0000000000..b28943e074
--- /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 0000000000..ff0dbf9745
--- /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) *)