Merge branch 'master'.

57 files changed, 1553 insertions, 206 deletions

diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v
index 0be859edd..7fae32871 100644
--- a/test-suite/bugs/closed/2310.v
+++ b/test-suite/bugs/closed/2310.v
@@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a.
    (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either
    leave P as subgoal or choose itself one solution *)
 
-intros. refine (Cons (cast H _ y)).
\ No newline at end of file
+  intros. Fail refine (Cons (cast H _ y)).
+  Unset Solve Unification Constraints. (* Keep the unification constraint around *)
+  refine (Cons (cast H _ y)).
+  intros.
+  refine (Nest (prod X X)). Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v
new file mode 100644
index 000000000..50d297807
--- /dev/null
+++ b/test-suite/bugs/closed/3441.v
@@ -0,0 +1,23 @@
+Axiom f : nat -> nat -> nat.
+Fixpoint do_n (n : nat) (k : nat) :=
+  match n with
+    | 0 => k
+    | S n' => do_n n' (f k k)
+  end.
+
+Notation big := (_ = _).
+Axiom k : nat.
+Goal True.
+Timeout 1 let H := fresh "H" in
+     let x := constr:(let n := 17 in do_n n = do_n n) in
+     let y := (eval lazy in x) in 
+     pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *)
+Timeout 1 let H := fresh "H" in
+     let x := constr:(let n := 17 in do_n n = do_n n) in
+     let y := (eval lazy in x) in
+     pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *)
+
+Timeout 1 Time let H := fresh "H" in
+     let x := constr:(let n := 17 in do_n n = do_n n) in
+     let y := (eval lazy in x) in
+     assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index fcdfa0057..9ed0926a6 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -1,4 +1,3 @@
-Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
 Require Coq.Setoids.Setoid.
 Import Coq.Setoids.Setoid.
@@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops.
 Local Existing Instance ILFun_ILogic.
 Definition catOP (P Q: OPred) : OPred := admit.
 Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
-admit.
+apply admit.
 Defined.
 Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
 Class IsPointed (T : Type) := point : T.
@@ -69,8 +68,27 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     pose P;
     refine (P _ _)
   end; unfold Basics.flip.
-  2: solve [ apply reflexivity ].
-  Undo.
-  2: reflexivity. (* Toplevel input, characters 18-29:
-Error:
-Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
+  Focus 2.
+  Set Typeclasses Debug.
+  Set Typeclasses Legacy Resolution.
+  apply reflexivity.
+  (* Debug: 1.1: apply @IsPointed_catOP on
+(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0))
+Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0))
+Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x))
+Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails)
+Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities
+Debug: Backtracking after apply @Equivalence_Reflexive
+Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails)
+Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails)
+Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
+*)
+  Undo. Unset Typeclasses Legacy Resolution.
+  Test Typeclasses Unique Solutions.
+  Test Typeclasses Unique Instances.
+  Show Existentials.
+  Set Typeclasses Debug Verbosity 2.
+  Set Printing All.
+  (* As in 8.5, allow a shelved subgoal to remain *)
+  apply reflexivity.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index 495e67e09..f5a22bd50 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -650,4 +650,5 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
 
   Grab Existential Variables.
   subst_body; simpl.
-  refine (all_behead (projT2 _)).
+  Fail refine (all_behead (projT2 _)).
+  Unset Solve Unification Constraints. refine (all_behead (projT2 _)).
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 8dadc2419..efa432526 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +46,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +109,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +121,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
new file mode 100644
index 000000000..ffd33d381
--- /dev/null
+++ b/test-suite/bugs/closed/4095.v
@@ -0,0 +1,87 @@
+(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Require Import Coq.Setoids.Setoid.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Ltac admit := apply admit.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+Local Existing Instance ILFun_Ops.
+Local Existing Instance ILFun_ILogic.
+Definition catOP (P Q: OPred) : OPred := admit.
+Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
+admit.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end.
+  Undo.
+  Fail lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
+    set(p:=P)
+  end. (* Toplevel input, characters 15-182:
+Error: Cannot infer an instance of type
+"PointedOPred" for the variable p in environment:
+T : Type
+O0 : T -> OPred
+O1 : T -> PointedOPred
+tr : T -> T
+O2 : PointedOPred
+x0 : T
+H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v
index b97a8ce64..3189685ec 100644
--- a/test-suite/bugs/closed/4416.v
+++ b/test-suite/bugs/closed/4416.v
@@ -1,3 +1,4 @@
 Goal exists x, x.
+Unset Solve Unification Constraints.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4708.v b/test-suite/bugs/closed/4708.v
new file mode 100644
index 000000000..ad2e58100
--- /dev/null
+++ b/test-suite/bugs/closed/4708.v
@@ -0,0 +1,8 @@
+(*Doc, it hurts when I poke myself.*)
+
+Notation "'" := 1. (* was:
+Setting notation at level 0.
+Toplevel input, characters 0-18:
+> Notation "'" := 1.
+> ^^^^^^^^^^^^^^^^^^
+Anomaly: Uncaught exception Invalid_argument("index out of bounds"). Please report. *)
diff --git a/test-suite/bugs/closed/4718.v b/test-suite/bugs/closed/4718.v
new file mode 100644
index 000000000..12a4e8fc1
--- /dev/null
+++ b/test-suite/bugs/closed/4718.v
@@ -0,0 +1,15 @@
+(*Congruence is weaker than reflexivity when it comes to higher level than necessary equalities:*)
+
+Goal @eq Set nat nat.
+congruence.
+Qed.
+
+Goal @eq Type nat nat.
+congruence. (*bug*)
+Qed.
+
+Variable T : Type.
+
+Goal @eq Type T T.
+congruence.
+Qed.
diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v
new file mode 100644
index 000000000..f047624c8
--- /dev/null
+++ b/test-suite/bugs/closed/4722.v
@@ -0,0 +1 @@
+(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *)
diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata
new file mode 120000
index 000000000..b38e66e75
--- /dev/null
+++ b/test-suite/bugs/closed/4722/tata
@@ -0,0 +1 @@
+toto
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
new file mode 100644
index 000000000..3854bbffd
--- /dev/null
+++ b/test-suite/bugs/closed/4727.v
@@ -0,0 +1,10 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
+    (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
+    o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
+Proof.
+  clear; intros ???????? inj H0 H1 H2.
+  destruct H2; intuition subst.
+  eapply inj in H1; [ | eauto ].
+  progress subst. (* should succeed, used to not succeed *)
+Abort.
diff --git a/test-suite/bugs/closed/4745.v b/test-suite/bugs/closed/4745.v
new file mode 100644
index 000000000..c090125e6
--- /dev/null
+++ b/test-suite/bugs/closed/4745.v
@@ -0,0 +1,35 @@
+(*I get an Anomaly in the following code.
+
+```*)
+Require Vector.
+
+Module M.
+  Lemma Vector_map_map :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v; simpl; auto using f_equal.
+  Qed.
+
+  Lemma Vector_map_map_transparent :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v; simpl; auto using f_equal.
+  Defined.
+  (* Anomaly: constant not found in kind_of_head: Coq.Vectors.Vector.t_ind. Please report. *)
+
+  (* strangely, explicitly passing the principle to induction works *)
+  Lemma Vector_map_map_transparent' :
+    forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n),
+      Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v.
+  Proof.
+    induction v using Vector.t_ind; simpl; auto using f_equal.
+  Defined.
+End M.
+(*```
+
+Changing any of the following things eliminates the Anomaly
+   * moving the lemma out of the module M to the top level
+   * proving the lemma as a Fixpoint instead of using induction
+   * proving the analogous lemma on lists instead of vectors*)
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 000000000..ae8ed0e6e
--- /dev/null
+++ b/test-suite/bugs/closed/4763.v
@@ -0,0 +1,13 @@
+Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
+Coercion is_true : bool >-> Sortclass.
+Global Instance: Transitive leb.
+Admitted.
+
+Goal forall x y z, leb x y -> leb y z -> True.
+  intros ??? H H'.
+  lazymatch goal with
+  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
+    => pose proof (transitivity H H' : is_true (R x z))
+  end.
+  exact I.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4772.v b/test-suite/bugs/closed/4772.v
new file mode 100644
index 000000000..c3109fa31
--- /dev/null
+++ b/test-suite/bugs/closed/4772.v
@@ -0,0 +1,6 @@
+
+Record TruncType := BuildTruncType {
+  trunctype_type : Type
+}.
+
+Fail Arguments BuildTruncType _ _ {_}. (* This should fail *)
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
index e884355fd..1e47f2957 100644
--- a/test-suite/bugs/closed/4863.v
+++ b/test-suite/bugs/closed/4863.v
@@ -3,14 +3,14 @@ Require Import Classes.DecidableClass.
 Inductive Foo : Set :=
 | foo1 | foo2.
 
-Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
 Proof.
   intros P H.
   refine (Build_Decidable _ (if H then true else false) _).
   intuition congruence.
 Qed.
 
-Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances.
 
 Goal forall (a b : Foo), {a=b}+{a<>b}.
 intros.
@@ -21,7 +21,8 @@ Check ltac:(abstract (exact I)) : True.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.
-split. typeclasses eauto. typeclasses eauto. Qed.
+split. typeclasses eauto. 
+typeclasses eauto. Qed.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.
diff --git a/test-suite/bugs/closed/4966.v b/test-suite/bugs/closed/4966.v
new file mode 100644
index 000000000..bd93cdc85
--- /dev/null
+++ b/test-suite/bugs/closed/4966.v
@@ -0,0 +1,10 @@
+(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *)
+
+Axiom proof_admitted : False.
+Hint Extern 0 => case proof_admitted : unused.
+Ltac do_tac tac := tac.
+
+Goal False.
+  Set Ltac Profiling.
+  Fail solve [ do_tac auto ].
+Abort.
diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v
new file mode 100644
index 000000000..684dba196
--- /dev/null
+++ b/test-suite/bugs/closed/5149.v
@@ -0,0 +1,47 @@
+Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x.
+intros.
+eexists.
+rewrite <- H.
+eassumption.
+Qed.
+
+Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) 
+            (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : 
+flat_type -> Type)
+            (v v' : interp_flat_type1 t'),
+    v = v' ->
+    forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0)
+           (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> 
+interp_flat_type0 t0)
+           (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t))
+           (x' : interp_flat_type1 (Tbase t)) (T : Type)
+           (flatten_binding_list : forall t0 : flat_type,
+               interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T)
+           (P : T -> list T -> Prop) (prod : Type -> Type -> Type)
+           (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) 
+(interp_flat_type1 (Tbase x0)) -> T)
+           (pair : forall A B : Type, A -> B -> prod A B),
+      P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x'))
+        (flatten_binding_list t' (SmartVarVar t' v') v) ->
+      (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 
+t'0)
+              (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)),
+          P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 
+x'0))
+            (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf 
+(Tbase t0) x0 = x'0) ->
+      interpf (Tbase t) x = x'.
+Proof.
+  intros ?????????????????????? interpf_SmartVarVar.
+  solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail 
+"too early".
+  Undo.
+  (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *)
+  Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ].
+  solve [eapply interpf_SmartVarVar; subst; eassumption].
+  Undo.
+  Unset Solve Unification Constraints.
+  (* User control of when constraints are solved *)
+  solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ].
+Qed.
+
diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v
new file mode 100644
index 000000000..261092ee6
--- /dev/null
+++ b/test-suite/bugs/closed/5180.v
@@ -0,0 +1,64 @@
+Universes a b c ω ω'.
+Definition Typeω := Type@{ω}.
+Definition Type2 : Typeω := Type@{c}.
+Definition Type1 : Type2 := Type@{b}.
+Definition Type0 : Type1 := Type@{a}.
+
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Definition Typei' (n : nat)
+  := match n return Type@{ω'} with
+     | 0 => Type0
+     | 1 => Type1
+     | 2 => Type2
+     | _ => Typeω
+     end.
+Definition TypeOfTypei' {n} (x : Typei' n) : Type@{ω'}
+  := match n return Typei' n -> Type@{ω'} with
+     | 0 | 1 | 2 | _ => fun x => x
+     end x.
+Definition Typei (n : nat) : Typei' (S n)
+  := match n return Typei' (S n) with
+     | 0 => Type0
+     | 1 => Type1
+     | _ => Type2
+     end.
+Definition TypeOfTypei {n} (x : TypeOfTypei' (Typei n)) : Type@{ω'}
+  := match n return TypeOfTypei' (Typei n) -> Type@{ω'} with
+     | 0 | 1 | _ => fun x => x
+     end x.
+Check Typei 0 : Typei 1.
+Check Typei 1 : Typei 2.
+
+Definition lift' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => (x : Type)
+     end.
+Definition lift'' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))
+  := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with
+     | 0 | 1 | 2 | _ => fun x => x
+     end. (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+Check (fun x : TypeOfTypei' (Typei 0) => TypeOfTypei' (Typei 1)).
+
+Definition lift''' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)).
+  refine match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n))  with
+         | 0 | 1 | 2 | _ => fun x => _
+         end.
+  exact x.
+  Undo.
+  (* The command has indeed failed with message:
+In environment
+n : nat
+x : TypeOfTypei' (Typei 0)
+The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
+ "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because  a < b).
+ *)
+  all:compute in *.
+  all:exact x.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5181.v b/test-suite/bugs/closed/5181.v
new file mode 100644
index 000000000..0e6d47197
--- /dev/null
+++ b/test-suite/bugs/closed/5181.v
@@ -0,0 +1,3 @@
+Definition foo (x y : nat) := x.
+Fail Arguments foo {_} : assert.
+
diff --git a/test-suite/bugs/closed/5188.v b/test-suite/bugs/closed/5188.v
new file mode 100644
index 000000000..e29ebfb4e
--- /dev/null
+++ b/test-suite/bugs/closed/5188.v
@@ -0,0 +1,5 @@
+Set Printing All.
+Axiom relation : forall (T : Type), Set.
+Axiom T : forall A (R : relation A), Set.
+Set Printing Universes.
+Parameter (A:_) (R:_) (e:@T A R).
diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v
new file mode 100644
index 000000000..7254afb42
--- /dev/null
+++ b/test-suite/bugs/closed/5198.v
@@ -0,0 +1,39 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 286 lines to 
+27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, 
+then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from 
+253 lines to 65 lines, then from 79 lines to 65 lines *)
+(* coqc version 8.6.0 (November 2016) compiled on Nov 12 2016 14:43:52 with 
+OCaml 4.02.3
+   coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-v8.6,v8.6 
+(7e992fa784ee6fa48af8a2e461385c094985587d) *)
+Axiom admit : forall {T}, T.
+Set Printing Implicit.
+Inductive nat := O | S (_ : nat).
+Axiom f : forall (_ _ : nat), nat.
+Class ZLikeOps (e : nat)
+  := { LargeT : Type ; SmallT : Type ; CarryAdd : forall (_ _ : LargeT), LargeT 
+}.
+Class BarrettParameters :=
+  { b : nat ; k : nat ; ops : ZLikeOps (f b k) }.
+Axiom barrett_reduce_function_bundled : forall {params : BarrettParameters}
+                                               (_ : @LargeT _ (@ops params)),
+    @SmallT _ (@ops params).
+
+Global Instance ZZLikeOps e : ZLikeOps (f (S O) e)
+  := { LargeT := nat ; SmallT := nat ; CarryAdd x y := y }.
+Definition SRep := nat.
+Local Instance x86_25519_Barrett : BarrettParameters
+  := { b := S O ; k := O ; ops := ZZLikeOps O }.
+Definition SRepAdd : forall (_ _ : SRep), SRep
+  := let v := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)) in
+     v.
+Definition SRepAdd' : forall (_ _ : SRep), SRep
+  := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)).
+(* Error:
+In environment
+x : SRep
+y : SRep
+The term "x" has type "SRep" while it is expected to have type
+ "@LargeT ?e ?ZLikeOps".
+ *)
diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v
new file mode 100644
index 000000000..ed137395f
--- /dev/null
+++ b/test-suite/bugs/closed/5203.v
@@ -0,0 +1,5 @@
+Goal True.
+  Typeclasses eauto := debug.
+  Fail solve [ typeclasses eauto ].
+  Fail typeclasses eauto.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/5208.v b/test-suite/bugs/closed/5208.v
new file mode 100644
index 000000000..b7a684a27
--- /dev/null
+++ b/test-suite/bugs/closed/5208.v
@@ -0,0 +1,222 @@
+Require Import Program.
+
+Require Import Coq.Strings.String.
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Numbers.BinNums.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Local Open Scope positive.
+
+Definition field : Type := positive.
+
+Section poly.
+  Universe U.
+
+  Inductive fields : Type :=
+  | pm_Leaf : fields
+  | pm_Branch : fields -> option Type@{U} -> fields -> fields.
+
+  Definition fields_left (f : fields) : fields :=
+    match f with
+    | pm_Leaf => pm_Leaf
+    | pm_Branch l _ _ => l
+    end.
+
+  Definition fields_right (f : fields) : fields :=
+    match f with
+    | pm_Leaf => pm_Leaf
+    | pm_Branch _ _ r => r
+    end.
+
+  Definition fields_here (f : fields) : option Type@{U} :=
+    match f with
+    | pm_Leaf => None
+    | pm_Branch _ s _ => s
+    end.
+
+  Fixpoint fields_get (p : field) (m : fields) {struct p} : option Type@{U} :=
+    match p with
+      | xH => match m with
+                | pm_Leaf => None
+                | pm_Branch _ x _ => x
+              end
+      | xO p' => fields_get p' match m with
+                               | pm_Leaf => pm_Leaf
+                               | pm_Branch L _ _ => L
+                             end
+      | xI p' => fields_get p' match m with
+                               | pm_Leaf => pm_Leaf
+                               | pm_Branch _ _ R => R
+                             end
+    end.
+
+  Definition fields_leaf : fields := pm_Leaf.
+
+  Inductive member (val : Type@{U}) : fields -> Type :=
+  | pmm_H : forall L R, member val (pm_Branch L (Some val) R)
+  | pmm_L : forall (V : option Type@{U}) L R, member val L -> member val (pm_Branch L V R)
+  | pmm_R : forall (V : option Type@{U}) L R, member val R -> member val (pm_Branch L V R).
+  Arguments pmm_H {_ _ _}.
+  Arguments pmm_L {_ _ _ _} _.
+  Arguments pmm_R {_ _ _ _} _.
+
+  Fixpoint get_member (val : Type@{U}) p {struct p}
+  : forall m, fields_get p m = @Some Type@{U} val -> member val m :=
+    match p as p return forall m, fields_get p m = @Some Type@{U} val -> member@{U} val m with
+      | xH => fun m =>
+        match m as m return fields_get xH m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : None = @Some Type@{U} _ =>
+                       match pf in _ = Z return match Z with
+                                                | Some _ => _
+                                                | None => unit
+                                                end
+                       with
+                       | eq_refl => tt
+                       end
+        | pm_Branch _ None _ => fun pf : None = @Some Type@{U} _ =>
+                                  match pf in _ = Z return match Z with
+                                                           | Some _ => _
+                                                           | None => unit
+                                                           end
+                                  with
+                                  | eq_refl => tt
+                                  end
+        | pm_Branch _ (Some x) _ => fun pf : @Some Type@{U} x = @Some Type@{U} val =>
+                                      match eq_sym pf in _ = Z return member@{U} val (pm_Branch _ Z _) with
+                                      | eq_refl => pmm_H
+                                      end
+        end
+      | xO p' => fun m =>
+        match m as m return fields_get (xO p') m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val =>
+                       @get_member _ p' pm_Leaf pf
+        | pm_Branch l _ _ => fun pf : fields_get p' l = @Some Type@{U} val =>
+                       @pmm_L _ _ _ _ (@get_member _ p' l pf)
+        end
+      | xI p' => fun m =>
+        match m as m return fields_get (xI p') m = @Some Type@{U} val -> member@{U} val m with
+        | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val =>
+                       @get_member _ p' pm_Leaf pf
+        | pm_Branch l _ r => fun pf : fields_get p' r = @Some Type@{U} val =>
+                               @pmm_R _ _ _ _ (@get_member _ p' r pf)
+        end
+    end.
+
+  Inductive record : fields -> Type :=
+  | pr_Leaf : record pm_Leaf
+  | pr_Branch : forall L R (V : option Type@{U}),
+      record L ->
+      match V return Type@{U} with
+        | None => unit
+        | Some t => t
+      end ->
+      record R ->
+      record (pm_Branch L V R).
+
+
+  Definition record_left {L} {V : option Type@{U}} {R}
+             (r : record (pm_Branch L V R)) : record L :=
+    match r in record z
+          return match z with
+                 | pm_Branch L _ _ => record L
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ l _ _ => l
+      | pr_Leaf => tt
+    end.
+Set Printing All.
+  Definition record_at {L} {V : option Type@{U}} {R} (r : record (pm_Branch L V R))
+  : match V return Type@{U} with
+    | None => unit
+    | Some t => t
+    end :=
+    match r in record z
+          return match z (* return ?X *) with
+                 | pm_Branch _ V _ => match V return Type@{U} with
+                                     | None => unit
+                                     | Some t => t
+                                     end
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ _ v _ => v
+      | pr_Leaf => tt
+    end.
+
+  Definition record_here {L : fields} (v : Type@{U}) {R : fields}
+             (r : record (pm_Branch L (@Some Type@{U} v) R)) : v :=
+    match r in record z
+          return match z return Type@{U} with
+                 | pm_Branch _ (Some v) _ => v
+                 | _ => unit
+                 end
+    with
+      | pr_Branch _ _ v _ => v
+      | pr_Leaf => tt
+    end.
+
+  Definition record_right {L V R} (r : record (pm_Branch L V R)) : record R :=
+    match r in record z return match z with
+                                  | pm_Branch _ _ R => record R
+                                  | _ => unit
+                                end
+    with
+      | pr_Branch _ _ _ r => r
+      | pr_Leaf => tt
+    end.
+
+  Fixpoint record_get {val : Type@{U}} {pm : fields} (m : member val pm) : record pm -> val :=
+    match m in member _ pm return record pm -> val with
+      | pmm_H => fun r => record_here r
+      | pmm_L m' => fun r => record_get m' (record_left r)
+      | pmm_R m' => fun r => record_get m' (record_right r)
+    end.
+
+  Fixpoint record_set {val : Type@{U}} {pm : fields} (m : member val pm) (x : val) {struct m}
+  : record pm -> record pm :=
+    match m in member _ pm return record pm -> record pm with
+    | pmm_H => fun r =>
+      pr_Branch (Some _)
+                (record_left r)
+                x
+                (record_right r)
+    | pmm_L m' => fun r =>
+      pr_Branch _
+                (record_set m' x (record_left r))
+                (record_at r)
+                (record_right r)
+    | pmm_R m' => fun r =>
+      pr_Branch _ (record_left r)
+                (record_at r)
+                (record_set m' x (record_right r))
+    end.
+End poly.
+Axiom cheat : forall {A}, A.
+Lemma record_get_record_set_different:
+  forall (T: Type) (vars: fields)
+    (pmr pmw: member T vars)
+    (diff: pmr <> pmw)
+    (r: record vars) (val: T),
+    record_get pmr (record_set pmw val r) = record_get pmr r.
+Proof.
+  intros.
+  revert pmr diff r val.
+  induction pmw; simpl; intros.
+  - dependent destruction pmr.
+    + congruence.
+    + auto.
+    + auto.
+  - dependent destruction pmr.
+    + auto.
+    + simpl. apply IHpmw. congruence.
+    + auto.
+  - dependent destruction pmr.
+    + auto.
+    + auto.
+    + simpl. apply IHpmw. congruence.
+Qed.
diff --git a/test-suite/bugs/closed/5277.v b/test-suite/bugs/closed/5277.v
new file mode 100644
index 000000000..7abc38bfc
--- /dev/null
+++ b/test-suite/bugs/closed/5277.v
@@ -0,0 +1,11 @@
+(* Scheme Equality not robust wrt names *)
+
+Module A1.
+  Inductive A (T : Type) := C (a : T).
+  Scheme Equality for A. (* success *)
+End A1.
+
+Module A2.
+  Inductive A (x : Type) := C (a : x).
+  Scheme Equality for A. 
+End A2.
diff --git a/test-suite/bugs/closed/5322.v b/test-suite/bugs/closed/5322.v
new file mode 100644
index 000000000..01aec8f29
--- /dev/null
+++ b/test-suite/bugs/closed/5322.v
@@ -0,0 +1,14 @@
+(* Regression in computing types of branches in "match" *)
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := a : op Unit Unit.
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2.
+  refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with
+         | _ => _
+         end.
diff --git a/test-suite/bugs/closed/5323.v b/test-suite/bugs/closed/5323.v
new file mode 100644
index 000000000..295b7cd9f
--- /dev/null
+++ b/test-suite/bugs/closed/5323.v
@@ -0,0 +1,26 @@
+(* Revealed a missing re-consideration of postponed problems *)
+
+Module A.
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type 
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := .
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2
+  := match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with end.
+End A.
+
+(* A shorter variant *)
+Module B.
+Inductive exprf (op : unit -> Type) : Type :=
+| A : exprf op
+| Op tR (opc : op tR) (args : exprf op) : exprf op.
+Inductive op : unit -> Type := .
+Definition bound_op (dst2 : unit) (opc2 : op dst2)
+  : forall (args2 : exprf op), Op op dst2 opc2 args2 = A op
+  := match opc2 in op h return (forall args2 : exprf ?[U], Op ?[V] ?[I] opc2 args2 = A op) with end.
+End B.
diff --git a/test-suite/bugs/closed/5331.v b/test-suite/bugs/closed/5331.v
new file mode 100644
index 000000000..28743736d
--- /dev/null
+++ b/test-suite/bugs/closed/5331.v
@@ -0,0 +1,11 @@
+(* Checking no anomaly on some unexpected intropattern *)
+
+Ltac ih H := induction H as H.
+Ltac ih' H H' := induction H as H'.
+
+Goal True -> True.
+Fail intro H; ih H.
+intro H; ih' H ipattern:([]).
+exact I.
+Qed.
+
diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v
index 5fbcfef4e..de60fd0ae 100644
--- a/test-suite/bugs/closed/HoTT_coq_117.v
+++ b/test-suite/bugs/closed/HoTT_coq_117.v
@@ -16,10 +16,29 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A,
 Admitted.
 
 Inductive Empty : Set := .
-Instance contr_from_Empty {_ : Funext} (A : Type) :
+Fail Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+Fail Instance contr_from_Empty {F : Funext} (A : Type) :
   Contr_internal (Empty -> A) :=
   BuildContr _
              (Empty_rect (fun _ => A))
              (fun f => path_forall _ f (fun x => Empty_rect _ x)).
+
+(** This could be disallowed, this uses the Funext argument *)
+Instance contr_from_Empty {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
+
+Instance contr_from_Empty' {_ : Funext} (A : Type) :
+  Contr_internal (Empty -> A) :=
+  BuildContr _
+             (Empty_rect (fun _ => A))
+             (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)).
 (* Toplevel input, characters 15-220:
 Anomaly: unknown meta ?190. Please report. *)
diff --git a/test-suite/bugs/opened/4701.v b/test-suite/bugs/opened/4701.v
new file mode 100644
index 000000000..9286f0f1f
--- /dev/null
+++ b/test-suite/bugs/opened/4701.v
@@ -0,0 +1,23 @@
+(*Suppose we have*)
+
+  Inductive my_if {A B} : bool -> Type :=
+  | then_case (_ : A) : my_if true
+  | else_case (_ : B) : my_if false.
+  Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10).
+
+(*then here are three inductive type declarations that work:*)
+
+  Inductive I1 :=
+  | i1 (x : I1).
+  Inductive I2 :=
+  | i2 (x : nat).
+  Inductive I3 :=
+  | i3 (b : bool) (x : If b Then I3 Else nat).
+
+(*and here is one that does not, despite being equivalent to [I3]:*)
+
+  Fail Inductive I4 :=
+  | i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in
+   "forall b : bool, (if b then I4 else nat) -> I4". *)
+
+(*I think this one should work.  I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*)
diff --git a/test-suite/bugs/opened/4717.v b/test-suite/bugs/opened/4717.v
new file mode 100644
index 000000000..9ad474672
--- /dev/null
+++ b/test-suite/bugs/opened/4717.v
@@ -0,0 +1,19 @@
+(*See below. They sometimes work, and sometimes do not. Is this a bug?*)
+
+Require Import Omega Psatz.
+
+Definition foo := nat.
+
+Goal forall (n : foo), 0 = n - n.
+Proof. intros. omega. (* works *) Qed.
+
+Goal forall (x n : foo), x = x + n - n.
+Proof.
+  intros.
+  Fail omega. (* Omega can't solve this system *)
+  Fail lia. (* Cannot find witness. *)
+  unfold foo in *.
+  omega. (* works *)
+Qed.
+
+(* Guillaume Melquiond: What matters is the equality. In the first case, it is @eq nat. In the second case, it is @eq foo. The same issue exists for ring and field. So it is not a bug, but it is worth fixing.*)
diff --git a/test-suite/bugs/opened/4721.v b/test-suite/bugs/opened/4721.v
new file mode 100644
index 000000000..1f184b393
--- /dev/null
+++ b/test-suite/bugs/opened/4721.v
@@ -0,0 +1,13 @@
+Variables S1 S2 : Set.
+
+Goal @eq Type S1 S2 -> @eq Type S1 S2.
+intro H.
+Fail tauto.
+assumption.
+Qed.
+
+(*This is in 8.5pl1, and Matthieq Sozeau says: "That's a regression in tauto indeed, which now requires exact equality of the universes, through a non linear goal pattern matching:
+match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible,
+with no additional universe constraints currently, but the two types are
+initially different. This can be fixed easily to allow the same flexibility
+as in 8.4 (or assumption) to unify the universes as well."*)
diff --git a/test-suite/bugs/opened/4728.v b/test-suite/bugs/opened/4728.v
new file mode 100644
index 000000000..230b4beb6
--- /dev/null
+++ b/test-suite/bugs/opened/4728.v
@@ -0,0 +1,72 @@
+(*I'd like the final [Check] in the following to work:*)
+
+Ltac fin_eta_expand :=
+  [ > lazymatch goal with
+      | [ H : _ |- _ ] => clear H
+      end..
+  | lazymatch goal with
+    | [ H : ?T |- ?T ]
+      => exact H
+    | [ |- ?G ]
+      => fail 0 "No hypothesis matching" G
+    end ];
+  let n := numgoals in
+  tryif constr_eq numgoals 0
+  then idtac
+  else fin_eta_expand.
+
+Ltac pre_eta_expand x :=
+  let T := type of x in
+  let G := match goal with |- ?G => G end in
+  unify T G;
+  unshelve econstructor;
+  destruct x;
+  fin_eta_expand.
+
+Ltac eta_expand x :=
+  let v := constr:(ltac:(pre_eta_expand x)) in
+  idtac v;
+  let v := (eval cbv beta iota zeta in v) in
+  exact v.
+
+Notation eta_expand x := (ltac:(eta_expand x)) (only parsing).
+
+Ltac partial_unify eqn :=
+  lazymatch eqn with
+  | ?x = ?x => idtac
+  | ?f ?x = ?g ?y
+    => partial_unify (f = g);
+       (tryif unify x y then
+           idtac
+         else tryif has_evar x then
+             unify x y
+           else tryif has_evar y then
+               unify x y
+             else
+               idtac)
+  | ?x = ?y
+    => idtac;
+       (tryif unify x y then
+           idtac
+         else tryif has_evar x then
+             unify x y
+           else tryif has_evar y then
+               unify x y
+             else
+               idtac)
+  end.
+
+Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" :=
+  let old_record' := eta_expand old_record in
+  partial_unify (old_record = new_record);
+  eexact new_record.
+
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Infix "*" := prod : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing).
+
+Check ltac:({ (1, 1) with {| snd := 2 |} }).
+Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *)
diff --git a/test-suite/bugs/opened/4755.v b/test-suite/bugs/opened/4755.v
new file mode 100644
index 000000000..9cc0d361e
--- /dev/null
+++ b/test-suite/bugs/opened/4755.v
@@ -0,0 +1,34 @@
+(*I'm not sure which behavior is better.  But if the change is intentional, it should be documented (I don't think it is), and it'd be nice if there were a flag for this, or if -compat 8.4 restored the old behavior.*)
+
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+                                 | Some k => Some k
+                                 | None => None
+                                 end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+Global Instance foo (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Global Instance bar (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> eq ==> Basics.flip Basics.impl)
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k.
+Proof.
+  intro.
+  pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+  Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *)
diff --git a/test-suite/bugs/opened/4771.v b/test-suite/bugs/opened/4771.v
new file mode 100644
index 000000000..396d74bdb
--- /dev/null
+++ b/test-suite/bugs/opened/4771.v
@@ -0,0 +1,22 @@
+Module Type Foo.
+
+Parameter Inline t : nat.
+
+End Foo.
+
+Module F(X : Foo).
+
+Tactic Notation "foo" ref(x) := idtac.
+
+Ltac g := foo X.t.
+
+End F.
+
+Module N.
+Definition t := 0 + 0.
+End N.
+
+Module K := F(N).
+
+(* Was
+Anomaly: Uncaught exception Not_found. Please report. *)
diff --git a/test-suite/bugs/opened/4778.v b/test-suite/bugs/opened/4778.v
new file mode 100644
index 000000000..633d158e9
--- /dev/null
+++ b/test-suite/bugs/opened/4778.v
@@ -0,0 +1,35 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+Definition f (v : option nat) := match v with
+                                 | Some k => Some k
+                                 | None => None
+                                 end.
+
+Axioms F G : (option nat -> option nat) -> Prop.
+Axiom FG : forall f, f None = None -> F f = G f.
+
+Axiom admit : forall {T}, T.
+
+Existing Instance eq_Reflexive.
+
+(* This instance is needed in 8.4, but is useless in 8.5 *)
+Global Instance foo (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl))
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+
+(*
+(* This is required in 8.5, but useless in 8.4 *)
+Global Instance bar (A := nat)
+  : Proper ((pointwise_relation _ eq)
+              ==> eq ==> eq ==> Basics.flip Basics.impl)
+           (@option_rect A (fun _ => Prop)) | 0.
+exact admit.
+Qed.
+*)
+
+Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. Proof.
+  intro.
+  pose proof (_ : (Proper (_ ==> eq ==> _) and)).
+  Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *)
diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/4781.v
new file mode 100644
index 000000000..8b651ac22
--- /dev/null
+++ b/test-suite/bugs/opened/4781.v
@@ -0,0 +1,94 @@
+Ltac force_clear :=
+  clear;
+  repeat match goal with
+         | [ H : _ |- _ ] => clear H
+         | [ H := _ |- _ ] => clearbody H
+         end.
+
+Class abstract_term {T} (x : T) := by_abstract_term : T.
+Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances.
+
+Goal True.
+(* These work: *)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in (let v : T := x in v)) in
+  pose x.
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(Set) with ?y => constr:(y) end in
+  pose x.
+(* This fails with an error: *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => constr:(y) end in
+  pose x. (* The command has indeed failed with message:
+Error: Variable y should be bound to a term. *)
+(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := match constr:(x) with ?y => y end in
+  pose x.
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := (eval cbv iota in x) in
+  pose x.
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let x := type of x in
+  pose x. (* should succeed *)
+  Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:(_ : abstract_term term) in
+  let x := type of x in
+  pose x. (* should succeed *)
+
+(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time.
+
+Even stranger, consider:*)
+  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x'.
+      let x := (eval cbv delta [x'] in x') in
+      pose x;
+      let z := (eval cbv iota in x) in
+      pose z.
+
+(*This works fine.  But if I change the period to a semicolon, I get:*)
+
+      Fail let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      pose x. (* Anomaly: Uncaught exception Not_found. Please report. *)
+ (* should succeed *)
+(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*)
+
+ Fail  let term := constr:(I) in
+  let T := type of term in
+  let x := constr:((_ : abstract_term term) : T) in
+  let y := (eval cbv iota in (let v : T := x in v)) in
+  pose y;
+    let x' := fresh "x'" in
+    pose x as x';
+      let x := (eval cbv delta [x'] in x') in
+      let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *)
+      idtac. (* should succeed *)
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 9d90de47c..b084ad498 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,6 +1,5 @@
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be
-specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
@@ -104,16 +103,15 @@ Expands to: Constant Top.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-Error: Arguments lists should agree on names they provide.
+Error: Argument lists should agree on the names they provide.
 The command has indeed failed with message:
 Error: Sequences of implicit arguments must be of different lengths.
 The command has indeed failed with message:
-Error: Arguments names must be distinct.
+Error: Some argument names are duplicated: F
 The command has indeed failed with message:
 Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Error: Extra arguments: y.
 The command has indeed failed with message:
-Error: To rename arguments the "rename" flag must be
-specified.
+Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to R.
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v
index 2d14c94ac..0cb331347 100644
--- a/test-suite/output/Arguments_renaming.v
+++ b/test-suite/output/Arguments_renaming.v
@@ -47,7 +47,7 @@ Check @myplus.
 
 Fail Arguments eq_refl {F g}, [H] k.
 Fail Arguments eq_refl {F}, [F] : rename.
-Fail Arguments eq_refl {F F}, [F] F.
+Fail Arguments eq_refl {F F}, [F] F : rename.
 Fail Arguments eq {F} x [z] : rename.
 Fail Arguments eq {F} x z y.
 Fail Arguments eq {R} s t.
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index a13ae4624..6879cbc3c 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -10,3 +10,5 @@ let fix f (m : nat) : nat := match m with
                              end in f 0
      : nat
 Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
+     = cofix inf : Inf := {| projS := inf |}
+     : Inf
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 8afa50ba5..fafb478ba 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,4 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   omega.
 Qed.
 
-
+CoInductive Inf := S { projS : Inf }.
+Definition expand_Inf (x : Inf) := S (projS x).
+CoFixpoint inf := S inf.
+Eval compute in inf.
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index fff86d6fa..6fa357a90 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -58,7 +58,7 @@ Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
 
-(** These tests show examples which do not factorize binders *)
+(** Test factorization of binders *)
 
 Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
 Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index c17b285bc..81fda176e 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,108 +1,108 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_S_n: forall n m : nat, S n <= S m -> n <= m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
 le_ind:
   forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
-le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
-le_n_S: forall n m : nat, n <= m -> S n <= S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-true: bool
 false: bool
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
-bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
-implb: bool -> bool -> bool
-xorb: bool -> bool -> bool
+true: bool
+is_true: bool -> Prop
 negb: bool -> bool
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-andb_true_intro:
-  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 eq_true: bool -> Prop
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
+implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
+xorb: bool -> bool -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+BoolSpec: Prop -> Prop -> bool -> Prop
+Nat.eqb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-is_true: bool -> Prop
-eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
-eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_rect_r:
   forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-BoolSpec: Prop -> Prop -> bool -> Prop
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
-Nat.even: nat -> bool
-Nat.odd: nat -> bool
-Nat.testbit: nat -> nat -> bool
-Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
+n_Sn: forall n : nat, n <> S n
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+O_S: forall n : nat, 0 <> S n
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+eq_S: forall x y : nat, x = y -> S x = S y
 eq_add_S: forall n m : nat, S n = S m -> n = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
 not_eq_S: forall n m : nat, n <> m -> S n <> S m
-O_S: forall n : nat, 0 <> S n
-n_Sn: forall n : nat, n <> S n
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+f_equal2_mult:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
 f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
-plus_n_Sm: forall n m : nat, S (n + m) = n + S m
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
-f_equal2_mult:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-h': newdef n <> n
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 h: n <> newdef n
 h': newdef n <> n
 h: n <> newdef n
+h': newdef n <> n
 h: n <> newdef n
 h: n <> newdef n
-h': ~ P n
 h: P n
 h': ~ P n
 h: P n
 h': ~ P n
 h: P n
+h': ~ P n
 h: P n
 h: P n
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 0d5924ec6..7038eac22 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,39 +1,39 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
 le_n_S: forall n m : nat, n <= m -> S n <= S m
-true: bool
+le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+Nat.eqb: nat -> nat -> bool
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 eq_add_S: forall n m : nat, S n = S m -> n = m
-f_equal2_plus:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
+eq_S: forall x y : nat, x = y -> S x = S y
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
 h: newdef n
 h: P n
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index f3c12effc..45ff5e73b 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,77 +1,77 @@
-true: bool
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-O: nat
-S: nat -> nat
-length: forall A : Type, list A -> nat
+Nat.eqb: nat -> nat -> bool
+Nat.two: nat
 Nat.zero: nat
 Nat.one: nat
-Nat.two: nat
-Nat.succ: nat -> nat
+O: nat
+Nat.double: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.div2: nat -> nat
+Nat.log2: nat -> nat
 Nat.pred: nat -> nat
+Nat.square: nat -> nat
+S: nat -> nat
+Nat.succ: nat -> nat
+Nat.ldiff: nat -> nat -> nat
 Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
 Nat.sub: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+length: forall A : Type, list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.div2: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.log2: nat -> nat
+Nat.double: nat -> nat
+Nat.pred: nat -> nat
+Nat.square: nat -> nat
+Nat.succ: nat -> nat
+S: nat -> nat
 Nat.ldiff: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-S: nat -> nat
-Nat.succ: nat -> nat
-Nat.pred: nat -> nat
-Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.div: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
-Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
-identity_refl: forall (A : Type) (a : A), identity a a
 iff_refl: forall A : Prop, A <-> A
+le_n: forall n : nat, n <= n
+identity_refl: forall (A : Type) (a : A), identity a a
 eq_refl: forall (A : Type) (x : A), x = x
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-le_n: forall n : nat, n <= n
-pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
+pair: forall A B : Type, A -> B -> A * B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
 h: n <> newdef n
 h: n <> newdef n
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 9949658c4..239edd1da 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1,4 +1,4 @@
 Ltac f H := split; [ a H | e H ]
 Ltac g := match goal with
-          | |- context [if ?X then _ else _] => case X
+          | |- context [ if ?X then _ else _ ] => case X
           end
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
new file mode 100644
index 000000000..a5b55a999
--- /dev/null
+++ b/test-suite/output/auto.out
@@ -0,0 +1,20 @@
+(* info auto: *)
+simple apply or_intror (in core).
+ intro.
+ assumption.
+Debug: (* debug auto: *)
+Debug: * assumption. (*fail*)
+Debug: * intro. (*fail*)
+Debug: * simple apply or_intror (in core). (*success*)
+Debug: ** assumption. (*fail*)
+Debug: ** intro. (*success*)
+Debug: ** assumption. (*success*)
+(* info eauto: *)
+simple apply or_intror.
+ intro.
+ exact H.
+Debug: (* debug eauto: *)
+Debug: 1 depth=5 
+Debug: 1.1 depth=4 simple apply or_intror
+Debug: 1.1.1 depth=4 intro
+Debug: 1.1.1.1 depth=4 exact H
diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v
new file mode 100644
index 000000000..a77b7b82e
--- /dev/null
+++ b/test-suite/output/auto.v
@@ -0,0 +1,11 @@
+(* testing info/debug auto/eauto *)
+
+Goal False \/ (True -> True).
+info_auto.
+Undo.
+debug auto.
+Undo.
+info_eauto.
+Undo.
+debug eauto.
+Qed.
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index c76fc74a0..b9413a4ac 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,4 +1,5 @@
 (* Set Printing Existential Instances. *)
+Unset Solve Unification Constraints.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.
 Goal True /\ True /\ True \/
              veeryyyyyyyyyyyyloooooooooooooonggidentifier =
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 3c696502c..465b3eb8c 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -41,6 +41,7 @@ Definition F (x:IND True) (A:Type) :=
 Theorem paradox : False.
   (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
 Fail Proof (F C False).
+Abort.
 
 (* Another bug found in November 2015 (a substitution was wrongly
    reversed at pretyping level) *)
@@ -61,3 +62,30 @@ Inductive Ind2 (b:=1) (c:nat) : Type :=
   Constr2 : Ind2 c.
 
 Eval vm_compute in Constr2 2.
+
+(* A bug introduced in ade2363 (similar to #5322 and #5324). This
+   commit started to see that some List.rev was wrong in the "var"
+   case of a pattern-matching problem but it failed to see that a
+   transformation from a list of arguments into a substitution was
+   still needed. *)
+
+(* The order of real arguments was made wrong by ade2363 in the "var"
+   case of the compilation of "match" *)
+
+Inductive IND2 : forall X Y:Type, Type :=
+  CONSTR2 : IND2 unit Empty_set.
+
+Check fun x:IND2 bool nat =>
+  match x in IND2 a b return a with
+  | y => _
+  end = true.
+
+(* From January 2017, using the proper function to turn arguments into
+   a substitution up to a context possibly containing let-ins, so that
+   the following, which was wrong also before ade2363, now works
+   correctly *)
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | y => (true,0)
+  end.
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index a75967411..6abfca4c3 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -38,3 +38,10 @@ Abort.
 Goal ~ identity 0 1.
 discriminate.
 Qed.
+
+(* Check discriminate on types with local definitions *)
+
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y, B x true = B y false -> False.
+discriminate.
+Qed.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 89b8bd7ac..1abe14774 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -1,4 +1,12 @@
 (* Checks syntax of Hints commands *)
+(* Old-style syntax *)
+Hint Resolve eq_refl eq_sym.
+Hint Resolve eq_refl eq_sym: foo.
+Hint Immediate eq_refl eq_sym.
+Hint Immediate eq_refl eq_sym: foo.
+Hint Unfold fst eq_sym.
+Hint Unfold fst eq_sym: foo.
+
 (* Checks that qualified names are accepted *)
 
 (* New-style syntax *)
@@ -8,13 +16,76 @@ Hint Unfold eq_sym: core.
 Hint Constructors eq: foo bar.
 Hint Extern 3 (_ = _) => apply eq_refl: foo bar.
 
-(* Old-style syntax *)
-Hint Resolve eq_refl eq_sym.
-Hint Resolve eq_refl eq_sym: foo.
-Hint Immediate eq_refl eq_sym.
-Hint Immediate eq_refl eq_sym: foo.
-Hint Unfold fst eq_sym.
-Hint Unfold fst eq_sym: foo.
+(* Extended new syntax with patterns *)
+Hint Resolve eq_refl | 4 (_ = _) : baz.
+Hint Resolve eq_sym eq_trans : baz.
+Hint Extern 3 (_ = _) => apply eq_sym : baz.
+
+Parameter pred : nat -> Prop.
+Parameter pred0 : pred 0.
+Parameter f : nat -> nat.
+Parameter predf : forall n, pred n -> pred (f n).
+
+(* No conversion on let-bound variables and constants in pred (the default) *)
+Hint Resolve pred0 | 1 (pred _) : pred.
+Hint Resolve predf | 0 : pred.
+
+(* Allow full conversion on let-bound variables and constants *)
+Create HintDb predconv discriminated.
+Hint Resolve pred0 | 1 (pred _) : predconv.
+Hint Resolve predf | 0 : predconv.
+
+Goal exists n, pred n.
+  eexists.
+  Fail Timeout 1 typeclasses eauto with pred.
+  Set Typeclasses Filtered Unification.
+  Set Typeclasses Debug Verbosity 2.
+  (* predf is not tried as it doesn't match the goal *)
+  typeclasses eauto with pred.
+Qed.
+
+Parameter predconv : forall n, pred n -> pred (0 + S n).
+
+(* The inferred pattern contains 0 + ?n, syntactic match will fail to see convertible
+ terms *)
+Hint Resolve pred0 : pred2.
+Hint Resolve predconv : pred2.
+
+(** In this database we allow predconv to apply to pred (S _) goals, more generally
+  than the inferred pattern (pred (0 + S _)). *)
+Create HintDb pred2conv discriminated.
+Hint Resolve pred0 : pred2conv.
+Hint Resolve predconv | 1 (pred (S _)) : pred2conv.
+
+Goal pred 3.
+  Fail typeclasses eauto with pred2.
+  typeclasses eauto with pred2conv.
+Abort.
+
+Set Typeclasses Filtered Unification.
+Set Typeclasses Debug Verbosity 2.
+Hint Resolve predconv | 1 (pred _) : pred.
+Hint Resolve predconv | 1 (pred (S _)) : predconv.
+Test Typeclasses Limit Intros.
+Goal pred 3.
+  (* predf is not tried as it doesn't match the goal *)
+  (* predconv is tried but fails as the transparent state doesn't allow
+     unfolding + *)
+  Fail typeclasses eauto with pred.
+  (* Here predconv succeeds as it matches (pred (S _)) and then
+     full unification is allowed *)
+  typeclasses eauto with predconv.
+Qed.
+
+(** The other way around: goal contains redexes instead of instances *)
+Goal exists n, pred (0 + n).
+  eexists.
+  (* predf is applied indefinitely *)
+  Fail Timeout 1 typeclasses eauto with pred.
+  (* pred0 (pred _) matches the goal *)
+  typeclasses eauto with predconv.
+Qed.
+
 
 (* Checks that local names are accepted *)
 Section A.
@@ -105,4 +176,4 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
 
   Timeout 1 Fail apply _. (* 0.06s *)
 Abort.
-End HintCut.
\ No newline at end of file
+End HintCut.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 9661b3bfa..f746def5c 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A.
    hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
 
 Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.
+
+
+Module TemplateProp.
+
+  (** Check lowering of a template universe polymorphic inductive to Prop *)
+  
+  Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Check Foo True : Prop.
+
+End TemplateProp.
+
+Module PolyNoLowerProp.
+
+  (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *)
+  
+  Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A.
+  
+  Fail Check Foo True : Prop.
+
+End PolyNoLowerProp.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index da2183841..78652fb64 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -150,6 +150,13 @@ match goal with
 end.
 Abort.
 
+(* Injection in the presence of local definitions *)
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y x' y', B x y = B x' y' -> y = y'.
+intros * [= H1 H2].
+exact H2.
+Qed.
+
 (* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 3eaa04144..6b1f0315b 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,79 @@
+Module onlyclasses.
+
+(* In 8.6 we still allow non-class subgoals *)
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Goal Foo * Foo.
+    split. shelve.
+    Set Typeclasses Debug.
+    typeclasses eauto.
+    Unshelve. typeclasses eauto.
+  Qed.
+
+  Module RJung.
+    Class Foo (x : nat).
+      
+      Instance foo x : x = 2 -> Foo x.
+      Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
+      Typeclasses eauto := debug.
+      Check (_ : Foo 2).
+
+
+      Fail Definition foo := (_ : 0 = 0).
+
+  End RJung.
+End onlyclasses.
+
+Module shelve_non_class_subgoals.
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Class Bar := {}.
+  Instance bar1 (f:Foo) : Bar := {}.
+
+  Typeclasses eauto := debug.
+  Set Typeclasses Debug Verbosity 2.
+  Goal Bar.
+    (* Solution has shelved subgoals (of non typeclass type) *)
+    typeclasses eauto.
+  Abort.
+End shelve_non_class_subgoals.
+
+Module RefineVsNoTceauto.
+
+  Class Foo (A : Type) := foo : A.
+  Instance: Foo nat := { foo := 0 }.
+  Instance: Foo nat := { foo := 42 }.
+  Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances.
+  Goal exists (f : Foo nat), @foo _ f = 0.
+  Proof.
+    unshelve (notypeclasses refine (ex_intro _ _ _)). 
+    Set Typeclasses Debug. Set Printing All.
+    all:once (typeclasses eauto).
+    Fail idtac. (* Check no subgoals are left *)
+    Undo 3.
+    (** In this case, the (_ = _) subgoal is not considered 
+        by typeclass resolution *)
+    refine (ex_intro _ _ _). Fail reflexivity.
+  Abort.
+
+End RefineVsNoTceauto.
+
+Module Leivantex2PR339.
+  (** Was a bug preventing to find hints associated with no pattern *)
+  Class Bar := {}.
+  Instance bar1 (t:Type) : Bar.
+  Hint Extern 0 => exact True : typeclass_instances.
+  Typeclasses eauto := debug.
+  Goal Bar.
+    Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto. (* Relies on resolution of a non-class subgoal *)
+    Undo 1.
+    typeclasses eauto with typeclass_instances.
+  Qed.
+End Leivantex2PR339.
+
 Module bt.
 Require Import Equivalence.
 
@@ -22,7 +98,7 @@ Goal exists R, @Refl nat R.
   solve [typeclasses eauto with foo].
 Qed.
 
-(* Set Typeclasses Compatibility "8.5". *)
+Set Typeclasses Compatibility "8.5".
 Parameter f : nat -> Prop.
 Parameter g : nat -> nat -> Prop.
 Parameter h : nat -> nat -> nat -> Prop.
@@ -32,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y.
 Hint Resolve a b c : mybase.
 Goal forall x y z, h x y z -> f x -> f y.
   intros.
-  Set Typeclasses Debug.
-  typeclasses eauto with mybase.
+  Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
   Unshelve.
 Abort.
 End bt.
@@ -62,7 +137,8 @@ Notation "'return' t" := (unit t).
 Class A `(e: T) := { a := True }.
 Class B `(e_: T) := { e := e_; sg_ass :> A e }.
 
-Set Typeclasses Debug.
+(* Set Typeclasses Debug. *)
+(* Set Typeclasses Debug Verbosity 2. *)
 
 Goal forall `{B T}, Prop.
   intros. apply a.
@@ -104,6 +180,40 @@ Section sec.
  Check U (fun x => e x) _.
 End sec.
 
+Module UniqueSolutions.
+  Set Typeclasses Unique Solutions.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := {}.
+    Instance eqb : Eq nat := {}.
+
+    Goal Eq nat.
+      try apply _.
+      Fail exactly_once typeclasses eauto.
+    Abort.
+End UniqueSolutions.
+
+
+Module UniqueInstances.
+  (** Optimize proof search on this class by never backtracking on (closed) goals
+      for it. *)
+  Set Typeclasses Unique Instances.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := _. constructor. Qed.
+    Instance eqb : Eq nat := {}.
+    Class Foo (A : Type) (e : Eq A) : Set.
+    Instance fooa : Foo _ eqa := {}.
+
+    Tactic Notation "refineu" open_constr(c) := unshelve refine c.
+
+    Set Typeclasses Debug.
+    Goal { e : Eq nat & Foo nat e }.
+      unshelve refineu (existT _ _ _).
+      all:simpl.
+      (** Does not backtrack on the (wrong) solution eqb *)
+      Fail all:typeclasses eauto.
+    Abort.
+End UniqueInstances.
+
 Module IterativeDeepening.
 
   Class A.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index bb1cf0654..3178c6fc1 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -1,3 +1,4 @@
+Require Import Program.Tactics.
 Module Backtracking.
   Class A := { foo : nat }.
 
@@ -8,7 +9,6 @@ Module Backtracking.
   Qed.
   
   Arguments foo A : clear implicits.
-  
   Example find42 : exists n, n = 42.
   Proof.
     eexists.
@@ -20,9 +20,13 @@ Module Backtracking.
     Fail reflexivity. 
     Undo 2.
     (* Without multiple successes it fails *)
-    Fail all:((once typeclasses eauto) + apply eq_refl).
+    Set Typeclasses Debug Verbosity 2.
+    Fail all:((once (typeclasses eauto with typeclass_instances))
+              + apply eq_refl).
     (* Does backtrack if other goals fail *)
-    all:((typeclasses eauto) + reflexivity).
+    all:[> typeclasses eauto + reflexivity .. ].
+    Undo 1.
+    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
     Show Proof.  
   Qed.
 
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 4db547f4e..160f2d9de 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -5,7 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Require Import List.
 
 Class A (A : Type).
   Instance an: A nat.
@@ -31,6 +30,8 @@ Defined.
 
 Hint Extern 0 (_ /\ _) => constructor : typeclass_instances.
 
+Existing Class and.
+
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
   eexists. eexists. typeclasses eauto.
@@ -46,7 +47,7 @@ Class C {T} `(a : A T) (t : T).
 Require Import Classes.Init.
 Hint Extern 0 { x : ?A & _ } =>
   unshelve class_apply @existT : typeclass_instances.
-
+Existing Class sigT.
 Set Typeclasses Debug.
 Instance can: C an 0.
 (* Backtrack on instance implementation *)
@@ -63,41 +64,6 @@ Proof.
 Defined.
   
 
-Parameter in_list : list (nat * nat) -> nat -> Prop.
-Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
-  ~ in_list l n.
-
-(* Hints Unfold not_in_list. *)
-
-Axiom
-  lem1 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
-
-Axiom
-  lem2 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
-
-Axiom
-  lem3 :
-    forall (l : list (nat * nat)) (n p q : nat),
-    not_in_list ((p, q) :: l) n -> not_in_list l n.
-
-Axiom
-  lem4 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
-
-Hint Resolve lem1 lem2 lem3 lem4: essai.
-
-Goal
-forall (l : list (nat * nat)) (n p q : nat),
-not_in_list ((p, q) :: l) n -> not_in_list l n.
-  intros.
-  eauto with essai.
-Qed.
-
 (* Example from Nicolas Magaud on coq-club - Jul 2000 *)
 
 Definition Nat : Set := nat.
@@ -126,6 +92,9 @@ Qed.
   Full backtracking on dependent subgoals.
  *)
 Require Import Coq.Classes.Init.
+
+Module NTabareau.
+
 Set Typeclasses Dependency Order.
 Unset Typeclasses Iterative Deepening.
 Notation "x .1" := (projT1 x) (at level 3).
@@ -149,7 +118,8 @@ Hint Extern 5 (Bar ?D.1) =>
 Hint Extern 5 (Qux ?D.1) =>
     destruct D; simpl : typeclass_instances.
 
-Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances.
+Hint Extern 1 myType =>
+  unshelve refine (fooTobar _ _).1 : typeclass_instances.
 
 Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
 
@@ -158,8 +128,94 @@ Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instance
 Unset Typeclasses Debug.
 Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
 Proof.
-  Time typeclasses eauto 10.
+  Time typeclasses eauto 10 with typeclass_instances.
   Undo. Set Typeclasses Iterative Deepening.
-  Time typeclasses eauto.
+  Time typeclasses eauto with typeclass_instances.
 Defined.
 
+End NTabareau.
+
+Module NTabareauClasses.
+
+Set Typeclasses Dependency Order.
+Unset Typeclasses Iterative Deepening.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+
+Parameter myType: Type. 
+Existing Class myType.
+
+Class Foo (a:myType) := {}.
+
+Class Bar (a:myType) := {}.
+
+Class Qux (a:myType) := {}.
+
+Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.
+
+Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}.
+
+Hint Extern 5 (Bar ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 5 (Qux ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances.
+
+Hint Extern 0 { x : _ & _ } =>
+  unshelve notypeclasses refine (existT _ _ _) : typeclass_instances.
+
+Unset Typeclasses Debug.
+
+Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
+Proof.
+  Time typeclasses eauto 10 with typeclass_instances.
+  Undo. Set Typeclasses Iterative Deepening.
+  (* Much faster in iteratove deepening mode *)
+  Time typeclasses eauto with typeclass_instances.
+Defined.
+
+End NTabareauClasses.
+
+
+Require Import List.
+
+Parameter in_list : list (nat * nat) -> nat -> Prop.
+Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
+  ~ in_list l n.
+
+(* Hints Unfold not_in_list. *)
+
+Axiom
+  lem1 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
+
+Axiom
+  lem2 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
+
+Axiom
+  lem3 :
+    forall (l : list (nat * nat)) (n p q : nat),
+    not_in_list ((p, q) :: l) n -> not_in_list l n.
+
+Axiom
+  lem4 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
+
+Hint Resolve lem1 lem2 lem3 lem4: essai.
+
+Goal
+forall (l : list (nat * nat)) (n p q : nat),
+not_in_list ((p, q) :: l) n -> not_in_list l n.
+  intros.
+  eauto with essai.
+Qed.