Imported Upstream version 8.5upstream/8.5

56 files changed, 1157 insertions, 54 deletions

diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v
index d41d2317..71d457b0 100644
--- a/test-suite/bugs/closed/3249.v
+++ b/test-suite/bugs/closed/3249.v
@@ -5,7 +5,7 @@ Ltac ret_and_left T :=
   lazymatch eval hnf in t with
     | ?a /\ ?b => constr:(proj1 T)
     | forall x : ?T', @?f x =>
-      constr:(fun x : T' => $(let fx := constr:(T x) in
+      constr:(fun x : T' => ltac:(let fx := constr:(T x) in
                               let t := ret_and_left fx in
-                              exact t)$)
+                              exact t))
   end.
diff --git a/test-suite/bugs/closed/3257.v b/test-suite/bugs/closed/3257.v
new file mode 100644
index 00000000..d8aa6a04
--- /dev/null
+++ b/test-suite/bugs/closed/3257.v
@@ -0,0 +1,5 @@
+Require Import Setoid Morphisms Basics.
+Lemma foo A B (P : B -> Prop) :
+  pointwise_relation _ impl (fun z => A -> P z) P.
+Proof.
+  Fail reflexivity.
diff --git a/test-suite/bugs/closed/3285.v b/test-suite/bugs/closed/3285.v
index 25162329..68e6b738 100644
--- a/test-suite/bugs/closed/3285.v
+++ b/test-suite/bugs/closed/3285.v
@@ -1,7 +1,7 @@
 Goal True.
 Proof.
 match goal with
-  | _ => let x := constr:($(fail)$) in idtac
+  | _ => let x := constr:(ltac:(fail)) in idtac
   | _ => idtac
 end.
 Abort.
diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v
index b08b7ab3..701480fc 100644
--- a/test-suite/bugs/closed/3286.v
+++ b/test-suite/bugs/closed/3286.v
@@ -6,20 +6,20 @@ Ltac make_apply_under_binders_in lem H :=
     | 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
+                              ltac:(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 ret := constr:(ltac:(match goal with
                                   | _ => (let H' := fresh in
                                           pose H as H';
                                           apply lem in H';
                                           exact (Some H'))
                                   | _ => exact (@None nat)
                                 end
-                               )$) in
+                               )) in
            let ret' := (eval cbv beta zeta in ret) in
            constr:(ret')
     | _ => constr:(@None nat)
diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v
index fb3791af..a5782298 100644
--- a/test-suite/bugs/closed/3314.v
+++ b/test-suite/bugs/closed/3314.v
@@ -1,9 +1,9 @@
 Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Definition Lift
-: $(let U1 := constr:(Type) in
+: ltac:(let U1 := constr:(Type) in
     let U0 := constr:(Type : U1) in
-    exact (U0 -> U1))$
+    exact (U0 -> U1))
   := fun T => T.
 
 Fail Check nat:Prop. (* The command has indeed failed with message:
diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index e6a50449..e3b5e943 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -8,7 +8,7 @@ Inductive foo : Type@{l} := bar : foo .
 Section MakeEq.
   Variables (a : foo@{i}) (b : foo@{j}).
 
-  Let t := $(let ty := type of b in exact ty)$.
+  Let t := ltac:(let ty := type of b in exact ty).
   Definition make_eq (x:=b) := a : t.
 End MakeEq.
 
diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v
index 63d5c7a5..dcf5394e 100644
--- a/test-suite/bugs/closed/3347.v
+++ b/test-suite/bugs/closed/3347.v
@@ -1,7 +1,7 @@
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *)
 Set Universe Polymorphism.
-Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
 Inductive Unit : Type1 := tt : Unit.
 Fail Check Unit : Set. (* [Check Unit : Set] should fail if [Type1] is defined correctly *)
diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v
index 14b66db3..a635285f 100644
--- a/test-suite/bugs/closed/3354.v
+++ b/test-suite/bugs/closed/3354.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing).
+Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing).
 Inductive Empty : Type1 := .
 Fail Check Empty : Set.
 (* Toplevel input, characters 15-116:
diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v
index 7e371162..88ae0305 100644
--- a/test-suite/bugs/closed/3467.v
+++ b/test-suite/bugs/closed/3467.v
@@ -1,5 +1,5 @@
 Module foo.
-  Notation x := $(exact I)$.
+  Notation x := ltac:(exact I).
 End foo.
 Module bar.
   Include foo.
diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v
index 03c60a8b..1321a859 100644
--- a/test-suite/bugs/closed/3487.v
+++ b/test-suite/bugs/closed/3487.v
@@ -1,4 +1,4 @@
-Notation bar := $(exact I)$.
+Notation bar := ltac:(exact I).
 Notation foo := bar (only parsing).
 Class baz := { x : False }.
 Instance: baz.
diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v
new file mode 100644
index 00000000..13a79cc8
--- /dev/null
+++ b/test-suite/bugs/closed/3554.v
@@ -0,0 +1 @@
+Example foo (f : forall {_ : Type}, Type) : Type.
diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v
index 2a282d22..9d37d1a2 100644
--- a/test-suite/bugs/closed/3682.v
+++ b/test-suite/bugs/closed/3682.v
@@ -3,4 +3,4 @@ Class Foo.
 Definition bar `{Foo} (x : Set) := Set.
 Instance: Foo.
 Definition bar1 := bar nat.
-Definition bar2 := bar $(admit)$.
+Definition bar2 := bar ltac:(admit).
diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v
index f7b13738..130d5777 100644
--- a/test-suite/bugs/closed/3684.v
+++ b/test-suite/bugs/closed/3684.v
@@ -1,5 +1,5 @@
 Require Import TestSuite.admit.
 Definition foo : Set.
 Proof.
-  refine ($(abstract admit)$).
+  refine (ltac:(abstract admit)).
 Qed.
diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v
index a5bea34a..7a0c3e6f 100644
--- a/test-suite/bugs/closed/3685.v
+++ b/test-suite/bugs/closed/3685.v
@@ -39,11 +39,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v
index b650920b..df5f6674 100644
--- a/test-suite/bugs/closed/3686.v
+++ b/test-suite/bugs/closed/3686.v
@@ -33,11 +33,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index df9f5f47..c24173ab 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -18,7 +18,7 @@ Top.8}
    Top.6
    Top.7
    Top.8 |=  *) *)
-Definition bar := $(let t := eval compute in foo in exact t)$.
+Definition bar := ltac:(let t := eval compute in foo in exact t).
 Check @bar. (* bar@{Top.13 Top.14 Top.15
 Top.16}
      : Type@{Top.16+1}
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 62137f0c..aad0bb44 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +47,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +111,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +124,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v
new file mode 100644
index 00000000..a50572ac
--- /dev/null
+++ b/test-suite/bugs/closed/3735.v
@@ -0,0 +1,4 @@
+Require Import Coq.Program.Tactics.
+Class Foo := { bar : Type }.
+Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *)
+Fail Program Lemma foo : Foo -> bar. 
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v
index 4dfb3380..c799d439 100644
--- a/test-suite/bugs/closed/3743.v
+++ b/test-suite/bugs/closed/3743.v
@@ -3,7 +3,7 @@
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
 Require Export Coq.Setoids.Setoid.
 
-Fail Add Parametric Relation A
+Add Parametric Relation A
 : A (@eq A)
     transitivity proved by transitivity
       as refine_rel.
diff --git a/test-suite/bugs/closed/3746.v b/test-suite/bugs/closed/3746.v
new file mode 100644
index 00000000..a9463f94
--- /dev/null
+++ b/test-suite/bugs/closed/3746.v
@@ -0,0 +1,92 @@
+
+(* Bug report #3746 : Include and restricted signature *)
+
+Module Type MT. Parameter p : nat. End MT.
+Module Type EMPTY. End EMPTY.
+Module Empty. End Empty.
+
+(* Include of an applied functor with restricted sig :
+   Used to create axioms (bug report #3746), now forbidden. *)
+
+Module F (X:EMPTY) : MT.
+ Definition p := 0.
+End F.
+
+Module InclFunctRestr.
+ Fail Include F(Empty).
+End InclFunctRestr.
+
+(* A few variants (indirect restricted signature), also forbidden. *)
+
+Module F1 := F.
+Module F2 (X:EMPTY) := F X.
+
+Module F3a (X:EMPTY). Definition p := 0. End F3a.
+Module F3 (X:EMPTY) : MT := F3a X.
+
+Module InclFunctRestrBis.
+ Fail Include F1(Empty).
+ Fail Include F2(Empty).
+ Fail Include F3(Empty).
+End InclFunctRestrBis.
+
+(* Recommended workaround: manual instance before the include. *)
+
+Module InclWorkaround.
+ Module Temp := F(Empty).
+ Include Temp.
+End InclWorkaround.
+
+Compute InclWorkaround.p.
+Print InclWorkaround.p.
+Print Assumptions InclWorkaround.p. (* Closed under the global context *)
+
+
+
+(* Related situations which are ok, just to check *)
+
+(* A) Include of non-functor with restricted signature :
+   creates a proxy to initial stuff *)
+
+Module M : MT.
+  Definition p := 0.
+End M.
+
+Module InclNonFunct.
+  Include M.
+End InclNonFunct.
+
+Definition check : InclNonFunct.p = M.p := eq_refl.
+Print Assumptions InclNonFunct.p. (* Closed *)
+
+
+(* B) Include of a module type with opaque content:
+   The opaque content is "copy-pasted". *)
+
+Module Type SigOpaque.
+ Definition p : nat. Proof. exact 0. Qed.
+End SigOpaque.
+
+Module InclSigOpaque.
+ Include SigOpaque.
+End InclSigOpaque.
+
+Compute InclSigOpaque.p.
+Print InclSigOpaque.p.
+Print Assumptions InclSigOpaque.p. (* Closed *)
+
+
+(* C) Include of an applied functor with opaque proofs :
+   opaque proof "copy-pasted" (and substituted). *)
+
+Module F' (X:EMPTY).
+ Definition p : nat. Proof. exact 0. Qed.
+End F'.
+
+Module InclFunctOpa.
+ Include F'(Empty).
+End InclFunctOpa.
+
+Compute InclFunctOpa.p.
+Print InclFunctOpa.p.
+Print Assumptions InclFunctOpa.p. (* Closed *)
diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v
new file mode 100644
index 00000000..108ebf59
--- /dev/null
+++ b/test-suite/bugs/closed/3807.v
@@ -0,0 +1,33 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Unset Universe Minimization ToSet.
+
+
+Definition foo : Type := nat.
+About foo.
+(* foo@{Top.1} : Type@{Top.1}*)
+(* Top.1 |=  *)
+
+Definition bar : foo -> nat.
+Admitted.
+About bar.
+(* bar@{Top.2} : foo@{Top.2} -> nat *)
+(* Top.2 |=  *)
+
+Lemma baz@{i} : foo@{i} -> nat.
+Proof.
+  exact bar.
+Defined.
+
+Definition bar'@{i} : foo@{i} -> nat.
+  intros f. exact 0.
+Admitted.
+About bar'.
+(* bar'@{i} : foo@{i} -> nat *)
+(* i |=  *)
+
+Axiom f@{i} : Type@{i}.
+(*
+*** [ f@{i} : Type@{i} ]
+(* i |=  *)
+*)
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/closed/3848.v
index a03e8ffd..c0ef02f1 100644
--- a/test-suite/bugs/opened/3848.v
+++ b/test-suite/bugs/closed/3848.v
@@ -19,4 +19,4 @@ Proof.
   refine (functor_forall
             (f^-1)
             (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
-Fail Defined. (* Error: Attempt to save an incomplete proof *)
+Defined. (* was: Error: Attempt to save an incomplete proof *)
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
index 4408ab88..070d1e9c 100644
--- a/test-suite/bugs/closed/3881.v
+++ b/test-suite/bugs/closed/3881.v
@@ -8,7 +8,7 @@ Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Axiom admit : forall {T}, T.
 Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity).
-Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
+Notation "g 'o' f" := ltac:(let g' := g in let f' := f in exact (fun x => g' (f' x))) (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
 Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope.
 Arguments eq_refl {_ _}.
 Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end.
diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
new file mode 100644
index 00000000..0aa029e7
--- /dev/null
+++ b/test-suite/bugs/closed/3923.v
@@ -0,0 +1,33 @@
+Module Type TRIVIAL.
+Parameter t:Type.
+End TRIVIAL.
+
+Module MkStore (Key : TRIVIAL).
+
+Module St : TRIVIAL.
+Definition t := unit.
+End St.
+
+End MkStore.
+
+
+
+Module Type CERTRUNTIMETYPES (B  : TRIVIAL).
+
+Parameter cert_fieldstore : Type.
+Parameter empty_fieldstore : cert_fieldstore.
+
+End CERTRUNTIMETYPES.
+
+
+
+Module MkCertRuntimeTypes (B  : TRIVIAL) : CERTRUNTIMETYPES B.
+
+Module FieldStore := MkStore B.
+
+Definition cert_fieldstore := FieldStore.St.t.
+Axiom empty_fieldstore : cert_fieldstore.
+
+End MkCertRuntimeTypes.
+
+Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)
diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v
new file mode 100644
index 00000000..ced13839
--- /dev/null
+++ b/test-suite/bugs/closed/3998.v
@@ -0,0 +1,24 @@
+Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }.
+Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *)
+
+Inductive I1 := C.
+Inductive I2 := .
+
+Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }.
+Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }.
+
+Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f.
+
+Class MapOps (M K : Set) := {
+  tgtTy: K -> Set;
+  update: M -> forall k:K, tgtTy k -> M
+}.
+
+Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F :=
+{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }.
+
+Axiom ex : RecordOf _ I1FieldType.
+
+Definition works := (fun ex' => update ex' C true) (update ex C false).
+Set Typeclasses Debug.
+Definition doesnt := update (update ex C false) C true.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v
index f808cb45..5932c9c5 100644
--- a/test-suite/bugs/closed/4116.v
+++ b/test-suite/bugs/closed/4116.v
@@ -110,7 +110,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
   Trunc_is_trunc : IsTrunc_internal n A.
 
 Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
-  refine (let __transparent_assert_hypothesis := (_ : type) in _);
+  unshelve refine (let __transparent_assert_hypothesis := (_ : type) in _);
   [
       | (
         let H := match goal with H := _ |- _ => constr:(H) end in
@@ -321,7 +321,7 @@ Section Grothendieck.
 
   Definition Gcategory : PreCategory.
   Proof.
-    refine (@Build_PreCategory
+    unshelve refine (@Build_PreCategory
               Pair
               (fun s d => Gmorphism s d)
               Gidentity
@@ -346,7 +346,7 @@ Section Grothendieck2.
   Instance iscategory_grothendieck_toset : IsCategory (Gcategory F).
   Proof.
     intros s d.
-    refine (isequiv_adjointify _ _ _ _).
+    unshelve refine (isequiv_adjointify _ _ _ _).
     {
       intro m.
       transparent assert (H' : (s.(c) = d.(c))).
diff --git a/test-suite/bugs/closed/4149.v b/test-suite/bugs/closed/4149.v
new file mode 100644
index 00000000..b81c680c
--- /dev/null
+++ b/test-suite/bugs/closed/4149.v
@@ -0,0 +1,4 @@
+Goal forall A, A -> Type.
+Proof.
+  intros; eauto.
+Qed.
diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v
new file mode 100644
index 00000000..3cdc4ada
--- /dev/null
+++ b/test-suite/bugs/closed/4256.v
@@ -0,0 +1,43 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Global Set Universe Polymorphism.
+Monomorphic Universe i.
+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.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+Notation "-1" := (trunc_S minus_two) (at level 0).
+
+Class IsPointed (A : Type) := point : A.
+Arguments point A {_}.
+
+Record pType :=
+  { pointed_type : Type ;
+    ispointed_type : IsPointed pointed_type }.
+Coercion pointed_type : pType >-> Sortclass.
+Existing Instance ispointed_type.
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+
+
+Record ooGroup :=
+  { classifying_space : pType@{i} }.
+
+Definition group_loops (X : pType)
+: ooGroup.
+Proof.
+  (** This works: *)
+  pose (x0 := point X).
+  pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)).
+  clear H x0.
+  (** But this doesn't: *)
+  pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)).
diff --git a/test-suite/bugs/closed/4273.v b/test-suite/bugs/closed/4273.v
new file mode 100644
index 00000000..591ea4b5
--- /dev/null
+++ b/test-suite/bugs/closed/4273.v
@@ -0,0 +1,9 @@
+
+  
+Set Primitive Projections.
+Record total2 (P : nat -> Prop) := tpair { pr1 : nat; pr2 : P pr1 }.
+Theorem onefiber' (q : total2 (fun y => y = 0)) : True.
+Proof. assert (foo:=pr2 _ q). simpl in foo.
+       destruct foo. (* Error: q is used in conclusion. *) exact I. Qed.
+
+Print onefiber'.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4284.v b/test-suite/bugs/closed/4284.v
new file mode 100644
index 00000000..0fff3026
--- /dev/null
+++ b/test-suite/bugs/closed/4284.v
@@ -0,0 +1,6 @@
+Set Primitive Projections.
+Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }.
+Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True.
+Proof.
+set (Q1 := total2 (fun f => pr1 P f = x)).
+set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)).
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 0623cf5b..43c9b512 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) :=
   let foo (A : Type@{j}) := A in foo B.
 
 Fail Check @setlt@{j Prop}.
-Check @setlt@{Prop j}.
-Check @setle@{Prop j}.
-
 Fail Definition foo := @setle@{j Prop}.
-Definition foo := @setle@{Prop j}.
+Check setlt@{Set i}.
+Check setlt@{Set j}.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v
new file mode 100644
index 00000000..3671c931
--- /dev/null
+++ b/test-suite/bugs/closed/4293.v
@@ -0,0 +1,7 @@
+Module Type Foo.
+Definition T := let X := Type in Type.
+End Foo.
+
+Module M : Foo.
+Definition T := let X := Type in Type.
+End M.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v
new file mode 100644
index 00000000..9895548c
--- /dev/null
+++ b/test-suite/bugs/closed/4363.v
@@ -0,0 +1,9 @@
+Set Printing Universes.
+Definition foo : Type.
+Proof.
+  assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat).
+  exact bar.
+Defined. (* Toplevel input, characters 0-8:
+Error:
+The term "(fun _ : Set => bar) foo_subproof" has type
+"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *)
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
new file mode 100644
index 00000000..5c23f840
--- /dev/null
+++ b/test-suite/bugs/closed/4400.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
+Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
+Set Printing Universes.
+Inductive Foo (I : Type -> Type) (A : Type) : Type :=
+| foo (B : Type) : A -> I B -> Foo I A.
+Definition Family := Type -> Type.
+Definition FooToo : Family -> Family := Foo.
+Definition optionize (I : Type -> Type) (A : Type) := option (I A).
+Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
+Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
+Definition barRec : Rec (optionize id) := {| rec := bar id |}.
+Inductive Empty {T} : T -> Prop := .
+Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
+nil)) (b : unit) :
+  Empty (a, b) -> False.
+Proof.
+  intro e.
+  dependent induction e.
+Qed.
diff --git a/test-suite/bugs/closed/4404.v b/test-suite/bugs/closed/4404.v
new file mode 100644
index 00000000..27b43a61
--- /dev/null
+++ b/test-suite/bugs/closed/4404.v
@@ -0,0 +1,4 @@
+Inductive Foo : Type -> Type := foo A : Foo A.
+Goal True.
+  remember Foo.
+
diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v
new file mode 100644
index 00000000..4b2aae0c
--- /dev/null
+++ b/test-suite/bugs/closed/4412.v
@@ -0,0 +1,4 @@
+Require Import Coq.Bool.Bool Coq.Setoids.Setoid.
+Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True.
+  intros.
+  Fail rewrite Bool.andb_true_iff in H.
diff --git a/test-suite/bugs/closed/4420.v b/test-suite/bugs/closed/4420.v
new file mode 100644
index 00000000..0e16cb23
--- /dev/null
+++ b/test-suite/bugs/closed/4420.v
@@ -0,0 +1,19 @@
+Module foo.
+  Context (Char : Type).
+  Axiom foo : Type -> Type.
+  Goal foo Char = foo Char.
+    change foo with (fun x => foo x).
+    cbv beta.
+    reflexivity.
+  Defined. 
+End foo.
+
+Inductive foo (A : Type) : Prop := I. (*Top.1*)
+Lemma bar : foo Type. (*Top.3*)
+Proof.
+  Set Printing Universes.
+change foo with (fun x : Type => foo x). (*Top.4*)
+cbv beta.
+apply I. (* I Type@{Top.3} : (fun x : Type@{Top.4} => foo x) Type@{Top.3} *)
+Defined.
+
diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v
new file mode 100644
index 00000000..bf0e570a
--- /dev/null
+++ b/test-suite/bugs/closed/4429.v
@@ -0,0 +1,31 @@
+Require Import Arith.Compare_dec.
+Require Import Unicode.Utf8.
+
+Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
+  match n with
+    | O    => x
+    | S n' => f (my_nat_iter n' f x)
+  end.
+
+Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
+  match mn with
+    | (0, 0)       => 0
+    | (0, S n')    => S n'
+    | (S m', 0)    => S m'
+    | (S m', S n') =>
+      match le_gt_dec (S m') (S n') with
+        | left  _ => f (S m', S n' - S m')
+        | right _ => f (S m' - S n', S n')
+      end
+  end.
+
+Axiom max_correct_l : ∀ m n : nat, m <= max m n.
+Axiom max_correct_r : ∀ m n : nat, n <= max m n.
+
+Hint Resolve max_correct_l max_correct_r : arith.
+
+Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
+Proof.
+  intros.
+  Timeout 3 eauto with arith.
+Qed.
diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v
new file mode 100644
index 00000000..9eeb8646
--- /dev/null
+++ b/test-suite/bugs/closed/4433.v
@@ -0,0 +1,29 @@
+Require Import Coq.Arith.Arith Coq.Init.Wf.
+Axiom proof_admitted : False.
+Goal exists x y z : nat, Fix
+                           Wf_nat.lt_wf
+                           (fun _ => nat -> nat)
+                           (fun x' f => match x' as x'0
+                                              return match x'0 with
+                                                       | 0 => True
+                                                       | S x'' => x'' < x'
+                                                     end
+                                                     -> nat -> nat
+                                        with
+                                          | 0 => fun _ _ => 0
+                                          | S x'' => f x''
+                                        end
+                                          (match x' with
+                                             | 0 => I
+                                             | S x'' => (Nat.lt_succ_diag_r _)
+                                           end))
+                           z
+                           y
+                         = 0.
+Proof.
+  do 3 (eexists; [ shelve.. | ]).
+  match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end.
+  case proof_admitted.
+  Unshelve.
+  all:constructor.
+Defined.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v
new file mode 100644
index 00000000..66dfa0e6
--- /dev/null
+++ b/test-suite/bugs/closed/4443.v
@@ -0,0 +1,31 @@
+Set Universe Polymorphism.
+
+Record TYPE@{i} := cType {
+  type : Type@{i};
+}.
+
+Definition PROD@{i j k}
+  (A : Type@{i})
+  (B : A -> Type@{j})
+  : TYPE@{k}.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+Local Unset Strict Universe Declaration.
+Definition PRODinj
+  (A : Type@{i})
+  (B : A -> Type)
+  : TYPE.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+  Monomorphic Universe i j.
+  Monomorphic Constraint j < i.
+Set Printing Universes.
+Check PROD@{i i i}.
+Check PRODinj@{i j}.
+Fail Check PRODinj@{j i}.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4453.v b/test-suite/bugs/closed/4453.v
new file mode 100644
index 00000000..009dd5e3
--- /dev/null
+++ b/test-suite/bugs/closed/4453.v
@@ -0,0 +1,8 @@
+
+Section Foo.
+Variable A : Type.
+Lemma foo : A -> True. now intros _. Qed.
+Goal Type -> True.
+rename A into B.
+intros A.
+Fail apply foo.
diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v
new file mode 100644
index 00000000..a32acf78
--- /dev/null
+++ b/test-suite/bugs/closed/4456.v
@@ -0,0 +1,647 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *)
+(* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0
+   coqtop version 8.5beta3 (November 2015) *)
+(* Variable P : forall n m : nat, n = m -> Prop. *)
+(* Axiom Prefl : forall n : nat, P n n eq_refl. *)
+Axiom proof_admitted : False.
+
+Tactic Notation "admit" := case proof_admitted.
+
+Require Coq.Program.Program.
+Require Coq.Strings.String.
+Require Coq.omega.Omega.
+Module Export Fiat_DOT_Common.
+Module Export Fiat.
+Module Common.
+Import Coq.Lists.List.
+Export Coq.Program.Program.
+
+Global Set Implicit Arguments.
+
+Global Coercion is_true : bool >-> Sortclass.
+Coercion bool_of_sum {A B} (b : sum A B) : bool := if b then true else false.
+
+Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type
+  := match ls return Type with
+     | nil => True
+     | x::xs => (P x * ForallT P xs)%type
+     end.
+Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type
+  := match ls with
+     | nil => P nil
+     | x::xs => (P (x::xs) * Forall_tails P xs)%type
+     end.
+
+End Common.
+
+End Fiat.
+
+End Fiat_DOT_Common.
+Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Core.
+Module Export Fiat.
+Module Export Parsers.
+Module Export StringLike.
+Module Export Core.
+Import Coq.Relations.Relation_Definitions.
+Import Coq.Classes.Morphisms.
+
+Local Coercion is_true : bool >-> Sortclass.
+
+Module Export StringLike.
+  Class StringLike {Char : Type} :=
+    {
+      String :> Type;
+      is_char : String -> Char -> bool;
+      length : String -> nat;
+      take : nat -> String -> String;
+      drop : nat -> String -> String;
+      get : nat -> String -> option Char;
+      unsafe_get : nat -> String -> Char;
+      bool_eq : String -> String -> bool;
+      beq : relation String := fun x y => bool_eq x y
+    }.
+
+  Arguments StringLike : clear implicits.
+  Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope.
+  Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope.
+  Local Open Scope string_like_scope.
+
+  Class StringLikeProperties (Char : Type) `{StringLike Char} :=
+    {
+      singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch';
+      singleton_exists : forall s, length s = 1 -> exists ch, s ~= [ ch ];
+      get_0 : forall s ch, take 1 s ~= [ ch ] <-> get 0 s = Some ch;
+      get_S : forall n s, get (S n) s = get n (drop 1 s);
+      unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch;
+      length_singleton : forall s ch, s ~= [ ch ] -> length s = 1;
+      bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s';
+      is_char_Proper :> Proper (beq ==> eq ==> eq) is_char;
+      length_Proper :> Proper (beq ==> eq) length;
+      take_Proper :> Proper (eq ==> beq ==> beq) take;
+      drop_Proper :> Proper (eq ==> beq ==> beq) drop;
+      bool_eq_Equivalence :> Equivalence beq;
+      bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str';
+      take_short_length : forall str n, n <= length str -> length (take n str) = n;
+      take_long : forall str n, length str <= n -> take n str =s str;
+      take_take : forall str n m, take n (take m str) =s take (min n m) str;
+      drop_length : forall str n, length (drop n str) = length str - n;
+      drop_0 : forall str, drop 0 str =s str;
+      drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str;
+      drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str);
+      take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str);
+      bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str'
+    }.
+Global Arguments StringLikeProperties _ {_}.
+End StringLike.
+
+End Core.
+
+End StringLike.
+
+End Parsers.
+
+End Fiat.
+
+End Fiat_DOT_Parsers_DOT_StringLike_DOT_Core.
+
+Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core.
+Module Export Fiat.
+Module Export Parsers.
+Module Export ContextFreeGrammar.
+Module Export Core.
+Import Coq.Strings.String.
+Import Coq.Lists.List.
+Export Fiat.Parsers.StringLike.Core.
+
+Section cfg.
+  Context {Char : Type}.
+
+  Section definitions.
+
+    Inductive item :=
+    | Terminal (_ : Char)
+    | NonTerminal (_ : string).
+
+    Definition production := list item.
+    Definition productions := list production.
+
+    Record grammar :=
+      {
+        Start_symbol :> string;
+        Lookup :> string -> productions;
+        Start_productions :> productions := Lookup Start_symbol;
+        Valid_nonterminals : list string;
+        Valid_productions : list productions := map Lookup Valid_nonterminals
+      }.
+  End definitions.
+
+  End cfg.
+
+Arguments item _ : clear implicits.
+Arguments production _ : clear implicits.
+Arguments productions _ : clear implicits.
+Arguments grammar _ : clear implicits.
+
+End Core.
+
+End ContextFreeGrammar.
+
+End Parsers.
+
+End Fiat.
+
+End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core.
+
+Module Export Fiat_DOT_Parsers_DOT_BaseTypes.
+Module Export Fiat.
+Module Export Parsers.
+Module Export BaseTypes.
+Import Coq.Arith.Wf_nat.
+
+Local Coercion is_true : bool >-> Sortclass.
+
+Section recursive_descent_parser.
+  Context {Char} {HSL : StringLike Char} {G : grammar Char}.
+
+  Class parser_computational_predataT :=
+    { nonterminals_listT : Type;
+      nonterminal_carrierT : Type;
+      of_nonterminal : String.string -> nonterminal_carrierT;
+      to_nonterminal : nonterminal_carrierT -> String.string;
+      initial_nonterminals_data : nonterminals_listT;
+      nonterminals_length : nonterminals_listT -> nat;
+      is_valid_nonterminal : nonterminals_listT -> nonterminal_carrierT -> bool;
+      remove_nonterminal : nonterminals_listT -> nonterminal_carrierT -> nonterminals_listT }.
+
+  Class parser_removal_dataT' `{predata : parser_computational_predataT} :=
+    { nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop
+      := ltof _ nonterminals_length;
+      nonterminals_length_zero : forall ls,
+                                   nonterminals_length ls = 0
+                                   -> forall nt, is_valid_nonterminal ls nt = false;
+      remove_nonterminal_dec : forall ls nonterminal,
+                                 is_valid_nonterminal ls nonterminal
+                                 -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls;
+      remove_nonterminal_noninc : forall ls nonterminal,
+                                    ~nonterminals_listT_R ls (remove_nonterminal ls nonterminal);
+      initial_nonterminals_correct : forall nonterminal,
+                                       is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) <-> List.In nonterminal (Valid_nonterminals G);
+      initial_nonterminals_correct' : forall nonterminal,
+                                       is_valid_nonterminal initial_nonterminals_data nonterminal <-> List.In (to_nonterminal nonterminal) (Valid_nonterminals G);
+      to_of_nonterminal : forall nonterminal,
+                            List.In nonterminal (Valid_nonterminals G)
+                            -> to_nonterminal (of_nonterminal nonterminal) = nonterminal;
+      of_to_nonterminal : forall nonterminal,
+                            is_valid_nonterminal initial_nonterminals_data nonterminal
+                            -> of_nonterminal (to_nonterminal nonterminal) = nonterminal;
+      ntl_wf : well_founded nonterminals_listT_R
+      := well_founded_ltof _ _;
+      remove_nonterminal_1
+      : forall ls ps ps',
+          is_valid_nonterminal (remove_nonterminal ls ps) ps'
+          -> is_valid_nonterminal ls ps';
+      remove_nonterminal_2
+      : forall ls ps ps',
+          is_valid_nonterminal (remove_nonterminal ls ps) ps' = false
+          <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }.
+
+  Class split_dataT :=
+    { split_string_for_production
+      : item Char -> production Char -> String -> list nat }.
+
+  Class boolean_parser_dataT :=
+    { predata :> parser_computational_predataT;
+      split_data :> split_dataT }.
+End recursive_descent_parser.
+
+End BaseTypes.
+
+End Parsers.
+
+End Fiat.
+
+End Fiat_DOT_Parsers_DOT_BaseTypes.
+
+Module Export Fiat_DOT_Common_DOT_List_DOT_Operations.
+Module Export Fiat.
+Module Export Common.
+Module Export List.
+Module Export Operations.
+
+Import Coq.Lists.List.
+
+Module Export List.
+  Section InT.
+    Context {A : Type} (a : A).
+
+    Fixpoint InT (ls : list A) : Set
+      := match ls return Set with
+           | nil => False
+           | b :: m => (b = a) + InT m
+         end%type.
+  End InT.
+
+  End List.
+
+End Operations.
+
+End List.
+
+End Common.
+
+End Fiat.
+
+End Fiat_DOT_Common_DOT_List_DOT_Operations.
+
+Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties.
+Module Export Fiat.
+Module Export Parsers.
+Module Export StringLike.
+Module Export Properties.
+
+Section String.
+  Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.
+
+  Lemma take_length {str n}
+  : length (take n str) = min n (length str).
+admit.
+Defined.
+
+  End String.
+
+End Properties.
+
+End StringLike.
+
+End Parsers.
+
+End Fiat.
+
+End Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties.
+
+Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties.
+Module Export Fiat.
+Module Export Parsers.
+Module Export ContextFreeGrammar.
+Module Export Properties.
+
+Local Open Scope list_scope.
+Definition production_is_reachableT {Char} (G : grammar Char) (p : production Char)
+  := { nt : _
+   & { prefix : _
+     & List.In nt (Valid_nonterminals G)
+       * List.InT
+            (prefix ++ p)
+            (Lookup G nt) } }%type.
+
+End Properties.
+
+End ContextFreeGrammar.
+
+End Parsers.
+
+End Fiat.
+
+End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties.
+
+Module Export Fiat_DOT_Parsers_DOT_MinimalParse.
+Module Export Fiat.
+Module Export Parsers.
+Module Export MinimalParse.
+Import Coq.Lists.List.
+Import Fiat.Parsers.ContextFreeGrammar.Core.
+
+Local Coercion is_true : bool >-> Sortclass.
+Local Open Scope string_like_scope.
+
+Section cfg.
+  Context {Char} {HSL : StringLike Char} {G : grammar Char}.
+  Context {predata : @parser_computational_predataT}
+          {rdata' : @parser_removal_dataT' _ G predata}.
+
+  Inductive minimal_parse_of
+  : forall (len0 : nat) (valid : nonterminals_listT)
+           (str : String),
+      productions Char -> Type :=
+  | MinParseHead : forall len0 valid str pat pats,
+                     @minimal_parse_of_production len0 valid str pat
+                     -> @minimal_parse_of len0 valid str (pat::pats)
+  | MinParseTail : forall len0 valid str pat pats,
+                     @minimal_parse_of len0 valid str pats
+                     -> @minimal_parse_of len0 valid str (pat::pats)
+  with minimal_parse_of_production
+  : forall (len0 : nat) (valid : nonterminals_listT)
+           (str : String),
+      production Char -> Type :=
+  | MinParseProductionNil : forall len0 valid str,
+                              length str = 0
+                              -> @minimal_parse_of_production len0 valid str nil
+  | MinParseProductionCons : forall len0 valid str n pat pats,
+                               length str <= len0
+                               -> @minimal_parse_of_item len0 valid (take n str) pat
+                               -> @minimal_parse_of_production len0 valid (drop n str) pats
+                               -> @minimal_parse_of_production len0 valid str (pat::pats)
+  with minimal_parse_of_item
+  : forall (len0 : nat) (valid : nonterminals_listT)
+           (str : String),
+      item Char -> Type :=
+  | MinParseTerminal : forall len0 valid str ch,
+                         str ~= [ ch ]
+                         -> @minimal_parse_of_item len0 valid str (Terminal ch)
+  | MinParseNonTerminal
+    : forall len0 valid str (nt : String.string),
+        @minimal_parse_of_nonterminal len0 valid str nt
+        -> @minimal_parse_of_item len0 valid str (NonTerminal nt)
+  with minimal_parse_of_nonterminal
+  : forall (len0 : nat) (valid : nonterminals_listT)
+           (str : String),
+      String.string -> Type :=
+  | MinParseNonTerminalStrLt
+    : forall len0 valid (nt : String.string) str,
+        length str < len0
+        -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt)
+        -> @minimal_parse_of (length str) initial_nonterminals_data str (Lookup G nt)
+        -> @minimal_parse_of_nonterminal len0 valid str nt
+  | MinParseNonTerminalStrEq
+    : forall len0 str valid nonterminal,
+        length str = len0
+        -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal)
+        -> is_valid_nonterminal valid (of_nonterminal nonterminal)
+        -> @minimal_parse_of len0 (remove_nonterminal valid (of_nonterminal nonterminal)) str (Lookup G nonterminal)
+        -> @minimal_parse_of_nonterminal len0 valid str nonterminal.
+
+End cfg.
+
+End MinimalParse.
+
+End Parsers.
+
+End Fiat.
+
+End Fiat_DOT_Parsers_DOT_MinimalParse.
+
+Module Export Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes.
+Module Export Fiat.
+Module Export Parsers.
+Module Export CorrectnessBaseTypes.
+Import Coq.Lists.List.
+Import Fiat.Parsers.ContextFreeGrammar.Core.
+Import Fiat_DOT_Common.Fiat.Common.
+Section general.
+  Context {Char} {HSL : StringLike Char} {G : grammar Char}.
+
+  Definition split_list_completeT_for {data : @parser_computational_predataT}
+             {len0 valid}
+             (it : item Char) (its : production Char)
+             (str : String)
+             (pf : length str <= len0)
+             (split_list : list nat)
+
+    := ({ n : nat
+              & (minimal_parse_of_item (G := G) (predata := data) len0 valid (take n str) it)
+                * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type)
+       -> ({ n : nat
+                 & (In (min (length str) n) (map (min (length str)) split_list))
+                   * (minimal_parse_of_item (G := G) len0 valid (take n str) it)
+                   * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type).
+
+  Definition split_list_completeT {data : @parser_computational_predataT}
+             (splits : item Char -> production Char -> String -> list nat)
+    := forall len0 valid str (pf : length str <= len0) nt,
+         is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt)
+         -> ForallT
+              (Forall_tails
+                 (fun prod
+                  => match prod return Type with
+                       | nil => True
+                       | it::its
+                         => @split_list_completeT_for data len0 valid it its str pf (splits it its str)
+                     end))
+              (Lookup G nt).
+
+  Class boolean_parser_completeness_dataT' {data : boolean_parser_dataT} :=
+    { split_string_for_production_complete
+      : split_list_completeT split_string_for_production }.
+End general.
+
+End CorrectnessBaseTypes.
+
+End Parsers.
+
+End Fiat.
+
+End Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes.
+
+Module Export Fiat.
+Module Export Parsers.
+Module Export ContextFreeGrammar.
+Module Export Valid.
+Export Fiat.Parsers.StringLike.Core.
+
+Section cfg.
+  Context {Char : Type} {HSL : StringLike Char} (G : grammar Char)
+          {predata : parser_computational_predataT}.
+
+  Definition item_valid (it : item Char)
+    := match it with
+         | Terminal _ => True
+         | NonTerminal nt' => is_true (is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt'))
+       end.
+
+  Definition production_valid pat
+    := List.Forall item_valid pat.
+
+  Definition productions_valid pats
+    := List.Forall production_valid pats.
+
+  Definition grammar_valid
+    := forall nt,
+         List.In nt (Valid_nonterminals G)
+         -> productions_valid (Lookup G nt).
+End cfg.
+
+End Valid.
+
+Section app.
+  Context {Char : Type} {HSL : StringLike Char} (G : grammar Char)
+          {predata : parser_computational_predataT}.
+
+  Lemma hd_production_valid
+        (it : item Char)
+        (its : production Char)
+        (H : production_valid (it :: its))
+  : item_valid it.
+admit.
+Defined.
+
+  Lemma production_valid_cons
+        (it : item Char)
+        (its : production Char)
+        (H : production_valid (it :: its))
+  : production_valid its.
+admit.
+Defined.
+
+  End app.
+
+Import Coq.Lists.List.
+Import Coq.omega.Omega.
+Import Fiat_DOT_Common.Fiat.Common.
+Import Fiat.Parsers.ContextFreeGrammar.Valid.
+Local Open Scope string_like_scope.
+
+Section recursive_descent_parser.
+  Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char).
+  Context {data : @boolean_parser_dataT Char _}
+          {cdata : @boolean_parser_completeness_dataT' Char _ G data}
+          {rdata : @parser_removal_dataT' _ G _}
+          {gvalid : grammar_valid G}.
+
+  Local Notation dec T := (T + (T -> False))%type (only parsing).
+
+  Local Notation iffT x y := ((x -> y) * (y -> x))%type (only parsing).
+
+  Lemma dec_prod {A B} (HA : dec A) (HB : dec B) : dec (A * B).
+admit.
+Defined.
+
+  Lemma dec_In {A} {P : A -> Type} (HA : forall a, dec (P a)) ls
+  : dec { a : _ & (In a ls * P a) }.
+admit.
+Defined.
+
+      Section item.
+        Context {len0 valid}
+                (str : String)
+                (str_matches_nonterminal'
+                 : nonterminal_carrierT -> bool)
+                (str_matches_nonterminal
+                 : forall nt : nonterminal_carrierT,
+                     dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))).
+
+        Section valid.
+          Context (Hmatches
+                   : forall nt,
+                       is_valid_nonterminal initial_nonterminals_data nt
+                       -> str_matches_nonterminal nt = str_matches_nonterminal' nt :> bool)
+                  (it : item Char)
+                  (Hvalid : item_valid it).
+
+          Definition parse_item'
+          : dec (minimal_parse_of_item (G := G) len0 valid str it).
+          Proof.
+            clear Hvalid.
+            refine (match it return dec (minimal_parse_of_item len0 valid str it) with
+                      | Terminal ch => if Sumbool.sumbool_of_bool (str ~= [ ch ])
+                                       then inl (MinParseTerminal _ _ _ _ _)
+                                       else inr (fun _ => !)
+                      | NonTerminal nt => if str_matches_nonterminal (of_nonterminal nt)
+                                          then inl (MinParseNonTerminal _)
+                                          else inr (fun _ => !)
+                    end);
+              clear str_matches_nonterminal Hmatches;
+              admit.
+          Defined.
+        End valid.
+
+        End item.
+        Context {len0 valid}
+                (parse_nonterminal
+                 : forall (str : String) (len : nat) (Hlen : length str = len) (pf : len <= len0) (nt : nonterminal_carrierT),
+                     dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))).
+
+        Lemma dec_in_helper {ls it its str}
+        : iffT {n0 : nat &
+                     (In (min (length str) n0) (map (min (length str)) ls) *
+                      minimal_parse_of_item (G := G) len0 valid (take n0 str) it *
+                      minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type}
+               {n0 : nat &
+                     (In n0 ls *
+                      (minimal_parse_of_item (G := G) len0 valid (take n0 str) it *
+                       minimal_parse_of_production (G := G) len0 valid (drop n0 str) its))%type}.
+admit.
+Defined.
+
+        Lemma parse_production'_helper {str it its} (pf : length str <= len0)
+        : dec {n0 : nat &
+                    (minimal_parse_of_item (G := G) len0 valid (take n0 str) it *
+                     minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type}
+          -> dec (minimal_parse_of_production (G := G) len0 valid str (it :: its)).
+admit.
+Defined.
+        Local Ltac t_parse_production_for := repeat
+                      match goal with
+              | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H
+              | _ => progress subst
+              | _ => solve [ constructor; assumption ]
+              | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H)
+              | [ H : minimal_parse_of_production _ _ _ (_::_) |- _ ] => (inversion H; clear H)
+              | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H'
+              | _ => progress simpl in *
+              | _ => discriminate
+              | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z))
+              | _ => solve [ eauto with nocore ]
+              | _ => solve [ apply Min.min_case_strong; omega ]
+              | _ => omega
+              | [ H : production_valid (_::_) |- _ ]
+                => let H' := fresh in
+                   pose proof H as H';
+                     apply production_valid_cons in H;
+                     apply hd_production_valid in H'
+            end.
+
+        Definition parse_production'_for
+                 (splits : item Char -> production Char -> String -> list nat)
+                 (Hsplits : forall str it its (Hreachable : production_is_reachableT G (it::its)) pf', split_list_completeT_for (len0 := len0) (G := G) (valid := valid) it its str pf' (splits it its str))
+                 (str : String)
+                 (len : nat)
+                 (Hlen : length str = len)
+                 (pf : len <= len0)
+                 (prod : production Char)
+                 (Hreachable : production_is_reachableT G prod)
+        : dec (minimal_parse_of_production (G := G) len0 valid str prod).
+        Proof.
+          revert prod Hreachable str len Hlen pf.
+          refine
+            ((fun pf_helper =>
+               list_rect
+                 (fun prod =>
+                    forall (Hreachable : production_is_reachableT G prod)
+                           (str : String)
+                           (len : nat)
+                           (Hlen : length str = len)
+                           (pf : len <= len0),
+                      dec (minimal_parse_of_production (G := G) len0 valid str prod))
+                 (
+                   fun Hreachable str len Hlen pf
+                   => match Utils.dec (beq_nat len 0) with
+                        | left H => inl _
+                        | right H => inr (fun p => _)
+                      end)
+                 (fun it its parse_production' Hreachable str len Hlen pf
+                  => parse_production'_helper
+                       _
+                       (let parse_item := (fun n pf => parse_item' (parse_nonterminal (take n str) (len := min n len) (eq_trans take_length (f_equal (min _) Hlen)) pf) it) in
+                        let parse_item := (fun n => parse_item n (Min.min_case_strong n len (fun k => k <= len0) (fun Hlen => (Nat.le_trans _ _ _ Hlen pf)) (fun Hlen => pf))) in
+                        let parse_production := (fun n => parse_production' (pf_helper it its Hreachable) (drop n str) (len - n) (eq_trans (drop_length _ _) (f_equal (fun x => x - _) Hlen)) (Nat.le_trans _ _ _ (Nat.le_sub_l _ _) pf)) in
+                        match dec_In
+                                (fun n => dec_prod (parse_item n) (parse_production n))
+                                (splits it its str)
+                        with
+                          | inl p => inl (existT _ (projT1 p) (snd (projT2 p)))
+                          | inr p
+                            => let pf' := (Nat.le_trans _ _ _ (Nat.eq_le_incl _ _ Hlen) pf) in
+                               let H := (_ : split_list_completeT_for (G := G) (len0 := len0) (valid := valid) it its str pf' (splits it its str)) in
+                               inr (fun p' => p (fst dec_in_helper (H p')))
+                        end)
+              )) _);
+            [ clear parse_nonterminal Hsplits splits rdata cdata
+            | clear parse_nonterminal Hsplits splits rdata cdata
+            | ..
+            | admit ].
+          abstract t_parse_production_for.
+          abstract t_parse_production_for.
+          abstract t_parse_production_for.
+          abstract t_parse_production_for.
+        Defined.
diff --git a/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v
new file mode 100644
index 00000000..c680518c
--- /dev/null
+++ b/test-suite/bugs/closed/4462.v
@@ -0,0 +1,7 @@
+Variables P Q : Prop.
+Axiom pqrw : P <-> Q.
+
+Require Setoid.
+
+Goal P -> Q.
+unshelve (rewrite pqrw).
diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v
new file mode 100644
index 00000000..6f8631d4
--- /dev/null
+++ b/test-suite/bugs/closed/4467.v
@@ -0,0 +1,15 @@
+(* Fixing missing test for variable shadowing *)
+
+Definition test (x y:bool*bool) :=
+  match x with
+  | (e as e1, (true) as e2)
+  | ((true) as e1, e as e2) =>
+    let '(e, b) := y in
+    e
+  | _ => true
+  end.
+
+Goal test (true,false) (true,true) = true.
+(* used to evaluate to "false = true" in 8.4 *)
+reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v
new file mode 100644
index 00000000..08a86330
--- /dev/null
+++ b/test-suite/bugs/closed/4480.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Definition proj (P Q : Prop) := P.
+
+Lemma foo (P : Prop) : proj P P = P.
+Admitted.
+Lemma trueI : True <-> True.
+Admitted.
+Goal True.
+  Fail setoid_rewrite foo.
+  Fail setoid_rewrite trueI.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v
new file mode 100644
index 00000000..f988539d
--- /dev/null
+++ b/test-suite/bugs/closed/4484.v
@@ -0,0 +1,10 @@
+(* Testing 8.5 regression with type classes not solving evars 
+   redefined while trying to solve them with the type class mechanism *)
+
+Class A := {}.
+Axiom foo : forall {ac : A}, bool.
+Lemma bar (ac : A) : True.
+Check (match foo as k return foo = k -> True with
+       | true => _
+       | false => _
+       end eq_refl).
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v
index e86b3be6..ea3347a8 100644
--- a/test-suite/bugs/closed/931.v
+++ b/test-suite/bugs/closed/931.v
@@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop.
 
 Goal Prop.
   refine (P _ _).
-  2:instantiate (1:=0).
+    instantiate (1:=0).
   trivial.
 Qed.
diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v
index db3b60ed..017780c1 100644
--- a/test-suite/bugs/closed/HoTT_coq_077.v
+++ b/test-suite/bugs/closed/HoTT_coq_077.v
@@ -30,7 +30,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B)
            (p : prod A B) : P p
   := u (fst p) (snd p).
 
-Notation typeof x := ($(let T := type of x in exact T)$) (only parsing).
+Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing).
 
 (* Check for eta *)
 Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect').
diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v
index 5fa16703..d77b9b63 100644
--- a/test-suite/bugs/closed/HoTT_coq_090.v
+++ b/test-suite/bugs/closed/HoTT_coq_090.v
@@ -84,7 +84,7 @@ Arguments transport {A} P {x y} p%path_scope u : simpl nomatch.
 Instance isequiv_path {A B : Type} (p : A = B)
   : IsEquiv (transport (fun X:Type => X) p) | 0.
 Proof.
-  refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
+  unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
   admit.
 Defined.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v
index 34112833..3535e6c4 100644
--- a/test-suite/bugs/closed/HoTT_coq_114.v
+++ b/test-suite/bugs/closed/HoTT_coq_114.v
@@ -1 +1 @@
-Inductive test : $(let U := type of Type in exact U)$ := t.
+Inductive test : ltac:(let U := type of Type in exact U) := t.
diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v
index 9e7d1eb5..33c408a2 100644
--- a/test-suite/bugs/opened/3248.v
+++ b/test-suite/bugs/opened/3248.v
@@ -3,7 +3,7 @@ Ltac ret_and_left f :=
   let T := type of f in
   lazymatch eval hnf in T with
     | ?T' -> _ =>
-      let ret := constr:(fun x' : T' => $(tac (f x'))$) in
+      let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in
       exact ret
     | ?T' => exact f
   end.
@@ -12,6 +12,6 @@ Goal forall A B : Prop, forall x y : A, True.
 Proof.
   intros A B x y.
   pose (f := fun (x y : A) => conj x y).
-  pose (a := $(ret_and_left f)$).
+  pose (a := ltac:(ret_and_left f)).
   Fail unify (a x y) (conj x y).
 Abort.
diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v
index 19ed787d..5f423136 100644
--- a/test-suite/bugs/opened/3277.v
+++ b/test-suite/bugs/opened/3277.v
@@ -4,4 +4,4 @@ Goal True.
   evarr _.
 Admitted.
 Goal True.
-  Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *)
+  Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *)
diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v
index ced535af..1c6deae9 100644
--- a/test-suite/bugs/opened/3278.v
+++ b/test-suite/bugs/opened/3278.v
@@ -1,8 +1,8 @@
 Module a.
   Check let x' := _ in
-             $(exact x')$.
+             ltac:(exact x').
 
-  Notation foo x := (let x' := x in $(exact x')$).
+  Notation foo x := (let x' := x in ltac:(exact x')).
 
   Fail Check foo _. (* Error:
 Cannot infer an internal placeholder of type "Type" in environment:
@@ -12,10 +12,10 @@ x' := ?42 : ?41
 End a.
 
 Module b.
-  Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I).
+  Notation foo x := (let x' := x in let y := (ltac:(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 let x' := _ in ltac:(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:
diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v
index 529cc737..66668930 100644
--- a/test-suite/bugs/opened/3304.v
+++ b/test-suite/bugs/opened/3304.v
@@ -1,3 +1,3 @@
-Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$.
+Fail Notation "( x , y , .. , z )" := ltac:(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/3459.v b/test-suite/bugs/opened/3459.v
index 9e6107b3..762611f7 100644
--- a/test-suite/bugs/opened/3459.v
+++ b/test-suite/bugs/opened/3459.v
@@ -7,9 +7,9 @@ Proof.
 (* This line used to fail with a Not_found up to some point, and then
    to produce an ill-typed term *)
 match goal with
-  | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in
+  | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in
                                                        clear x;
-                                                       exact r)$) in
+                                                       exact r)) in
                            pose y
 end.
 (* Add extra test for typability (should not fail when bug closed) *)
diff --git a/test-suite/bugs/opened/3554.v b/test-suite/bugs/opened/3554.v
deleted file mode 100644
index 422c5770..00000000
--- a/test-suite/bugs/opened/3554.v
+++ /dev/null
@@ -1 +0,0 @@
-Fail Example foo (f : forall {_ : Type}, Type) : Type.