From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 test-suite/success/Case13.v             |   8 +
 test-suite/success/CaseInClause.v       |   7 +
 test-suite/success/Compat84.v           |  19 +++
 test-suite/success/Hints.v              |  91 ++++++++++--
 test-suite/success/Inductive.v          |  21 +++
 test-suite/success/Injection.v          |  36 ++++-
 test-suite/success/MatchFail.v          |   8 +-
 test-suite/success/Notations.v          |  23 ++-
 test-suite/success/Notations2.v         |  92 ++++++++++++
 test-suite/success/PatternsInBinders.v  |  67 +++++++++
 test-suite/success/RecTutorial.v        |   6 +-
 test-suite/success/TacticNotation2.v    |  12 ++
 test-suite/success/TestRefine.v         |   2 +-
 test-suite/success/Typeclasses.v        | 188 +++++++++++++++++++++++-
 test-suite/success/apply.v              |   2 +-
 test-suite/success/auto.v               |  89 ++++++++++++
 test-suite/success/bigQ.v               |  66 +++++++++
 test-suite/success/bteauto.v            | 170 ++++++++++++++++++++++
 test-suite/success/cc.v                 |  20 +++
 test-suite/success/clear.v              |  18 +++
 test-suite/success/coindprim.v          |  85 ++++++++---
 test-suite/success/contradiction.v      |  32 ++++
 test-suite/success/decl_mode2.v         | 249 ++++++++++++++++++++++++++++++++
 test-suite/success/destruct.v           |   8 +-
 test-suite/success/eauto.v              | 199 ++++++++++++++++++++++---
 test-suite/success/eqdecide.v           |  12 ++
 test-suite/success/goal_selector.v      |  55 +++++++
 test-suite/success/induct.v             |  43 ++++++
 test-suite/success/intros.v             |  44 ++++++
 test-suite/success/keyedrewrite.v       |   3 +-
 test-suite/success/ltac.v               |  14 +-
 test-suite/success/ltacprof.v           |   8 +
 test-suite/success/onlyprinting.v       |   7 +
 test-suite/success/par_abstract.v       |  25 ++++
 test-suite/success/paralleltac.v        |  26 +++-
 test-suite/success/primitiveproj.v      |  18 +--
 test-suite/success/programequality.v    |  13 ++
 test-suite/success/remember.v           |  13 ++
 test-suite/success/setoid_test.v        |  13 ++
 test-suite/success/shrink_abstract.v    |  13 ++
 test-suite/success/shrink_obligations.v |  28 ++++
 test-suite/success/simpl_tuning.v       |   2 +-
 test-suite/success/specialize.v         |   8 +
 test-suite/success/ssrpattern.v         |  22 +++
 test-suite/success/subst.v              |  42 ++++++
 test-suite/success/univers.v            |  17 +++
 test-suite/success/vm_univ_poly.v       |  12 +-
 47 files changed, 1849 insertions(+), 107 deletions(-)
 create mode 100644 test-suite/success/Compat84.v
 create mode 100644 test-suite/success/Notations2.v
 create mode 100644 test-suite/success/PatternsInBinders.v
 create mode 100644 test-suite/success/TacticNotation2.v
 create mode 100644 test-suite/success/bigQ.v
 create mode 100644 test-suite/success/bteauto.v
 create mode 100644 test-suite/success/contradiction.v
 create mode 100644 test-suite/success/decl_mode2.v
 create mode 100644 test-suite/success/goal_selector.v
 create mode 100644 test-suite/success/ltacprof.v
 create mode 100644 test-suite/success/onlyprinting.v
 create mode 100644 test-suite/success/par_abstract.v
 create mode 100644 test-suite/success/programequality.v
 create mode 100644 test-suite/success/shrink_abstract.v
 create mode 100644 test-suite/success/shrink_obligations.v
 create mode 100644 test-suite/success/ssrpattern.v
 create mode 100644 test-suite/success/subst.v

(limited to 'test-suite/success')

diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index f14725a8..8f95484c 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with
                        | _ => 0
                        end).
 
+(* This one could eventually be solved, the "Fail" is just to ensure *)
+(* that it does not fail with an anomaly, as it did at some time *)
+Fail Check (fun x : I' 0 => match x return _ x with
+                       | C2' _ _ => 0
+                       | niln => 0
+                       | _ => 0
+                       end).
+
 (* Check insertion of coercions around matched subterm *)
 
 Parameter A:Set.
diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v
index 3679eead..6424fe92 100644
--- a/test-suite/success/CaseInClause.v
+++ b/test-suite/success/CaseInClause.v
@@ -20,3 +20,10 @@ Theorem foo : forall (n m : nat) (pf : n = m),
                 match pf in _ = N with 
                   | eq_refl => unit
                 end.
+
+(* Check redundant clause is removed *)
+Inductive I : nat * nat -> Type := C : I (0,0).
+Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end.
+
+(* An example of non-local inference of the type of an impossible case *)
+Check (fun y n (x:Vector.t nat (S n)) => match x with a::_ => a | _ => y end) 2.
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
new file mode 100644
index 00000000..db6348fa
--- /dev/null
+++ b/test-suite/success/Compat84.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+
+Goal True.
+  solve [ constructor 1 ]. Undo.
+  solve [ econstructor 1 ]. Undo.
+  solve [ constructor ]. Undo.
+  solve [ econstructor ]. Undo.
+  solve [ constructor (fail) ]. Undo.
+  solve [ econstructor (fail) ]. Undo.
+  split.
+Qed.
+
+Goal False \/ True.
+  solve [ constructor (constructor) ]. Undo.
+  solve [ econstructor (econstructor) ]. Undo.
+  solve [ constructor 2; constructor ]. Undo.
+  solve [ econstructor 2; econstructor ]. Undo.
+  right; esplit.
+Qed.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index f934a5c7..1abe1477 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.
@@ -100,9 +171,9 @@ Instance foo f :
 Proof.
   Fail Timeout 1 apply _. (* 3.7s *)
   
-Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ;
-  (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
+Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
+                 (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
 
   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 9661b3bf..f746def5 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 25e464d6..da218384 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -4,6 +4,7 @@ Require Eqdep_dec.
 
 (* Check that Injection tries Intro until *)
 
+Unset Structural Injection.
 Lemma l1 : forall x : nat, S x = S (S x) -> False.
  injection 1.
 apply n_Sn.
@@ -37,6 +38,7 @@ intros.
  injection H.
 exact (fun H => H).
 Qed.
+Set Structural Injection.
 
 (* Test injection as *)
 
@@ -65,7 +67,13 @@ Qed.
 Goal (forall x y : nat, x = y -> S x = S y) -> True.
 intros.
 einjection (H O).
-instantiate (1:=O).
+2:instantiate (1:=O).
+Abort.
+
+Goal (forall x y : nat, x = y -> S x = S y) -> True.
+intros.
+einjection (H O ?[y]) as H0.
+instantiate (y:=O).
 Abort.
 
 (* Test the injection intropattern *)
@@ -79,12 +87,21 @@ Qed.
 (* Basic case, using sigT *)
 
 Scheme Equality for nat.
+Unset Structural Injection.
 Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
   existT P n H1 = existT P n H2 -> H1 = H2.
 intros.
 injection H.
 intro H0. exact H0.
 Abort.
+Set Structural Injection.
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  existT P n H1 = existT P n H2 -> H1 = H2.
+intros.
+injection H as H0.
+exact H0.
+Abort.
 
 (* Test injection using K, knowing that an equality is decidable *)
 (* Basic case, using sigT, with "as" clause *)
@@ -118,7 +135,22 @@ intros * [= H].
 exact H.
 Abort.
 
-(* Injection does not projects at positions in Prop... allow it?
+(* Test the Keep Proof Equalities option. *)
+Set Keep Proof Equalities.
+Unset Structural Injection.
+
+Inductive pbool : Prop := Pbool1 | Pbool2.
+
+Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell.
+
+Goal Pbsc Pbool1 = Pbsc Pbool2 -> True.
+injection 1.
+match goal with
+ |- Pbool1 = Pbool2 -> True => idtac | |- True => fail
+end.
+Abort.
+
+(* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
 Goal forall p q : True\/True, c _ p = c _ q -> False.
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
index 7069bba4..8462d362 100644
--- a/test-suite/success/MatchFail.v
+++ b/test-suite/success/MatchFail.v
@@ -9,14 +9,14 @@ Require Export ZArithRing.
 Ltac compute_POS :=
   match goal with
   |  |- context [(Zpos (xI ?X1))] =>
-      let v := constr:X1 in
-      match constr:v with
+      let v := constr:(X1) in
+      match constr:(v) with
       | 1%positive => fail 1
       | _ =>  rewrite (BinInt.Pos2Z.inj_xI v)
       end
   |  |- context [(Zpos (xO ?X1))] =>
-      let v := constr:X1 in
-      match constr:v with
+      let v := constr:(X1) in
+      match constr:(v) with
       | 1%positive => fail 1
       | _ =>  rewrite (BinInt.Pos2Z.inj_xO v)
       end
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index b72a0674..07bbb60c 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -58,7 +58,7 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end).
 
 (* Check multi-tokens recursive notations *)
 
-Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).   
+Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).
 Check [ 0 ].
 Check [ 0 # ; 1 ].
 
@@ -107,3 +107,24 @@ Notation traverse_var f l := (traverse (fun l => f l) l).
 
 Notation "'intros' x" := (S x) (at level 0).
 Goal True -> True. intros H. exact H. Qed.
+
+(* Check absence of collision on ".." in nested notations with ".." *)
+Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
+
+(* Check that vector notations do not break Ltac [] (bugs #4785, #4733) *)
+Require Import Coq.Vectors.VectorDef.
+Import VectorNotations.
+Goal True. idtac; []. (* important for test: no space here *) constructor. Qed.
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
+Check |- {{ 0 }} 0.
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
new file mode 100644
index 00000000..9505a56e
--- /dev/null
+++ b/test-suite/success/Notations2.v
@@ -0,0 +1,92 @@
+(* This file is giving some examples about how implicit arguments and
+   scopes are treated when using abbreviations or notations, in terms
+   or patterns, or when using @ and parentheses in terms and patterns.
+
+The convention is:
+
+Constant foo with implicit arguments and scopes used in a term or a pattern:
+
+       foo      do not deactivate further arguments and scopes
+       @foo     deactivates further arguments and scopes
+       (foo x)  deactivates further arguments and scopes
+       (@foo x) deactivates further arguments and scopes
+
+Notations binding to foo:
+
+#   := foo      do not deactivate further arguments and scopes
+#   := @foo     deactivates further arguments and scopes
+# x := foo x    deactivates further arguments and scopes
+# x := @foo x   deactivates further arguments and scopes
+
+Abbreviations binding to foo:
+
+f   := foo      do not deactivate further arguments and scopes
+f   := @foo     deactivates further arguments and scopes
+f x := foo x    do not deactivate further arguments and scopes
+f x := @foo x   do not deactivate further arguments and scopes
+*)
+
+(* One checks that abbreviations and notations in patterns now behave like in terms *)
+
+Inductive prod' A : Type -> Type :=
+| pair' (a:A) B (b:B) (c:bool) : prod' A B.
+Arguments pair' [A] a%bool_scope [B] b%bool_scope c%bool_scope.
+Notation "0" := true : bool_scope.
+
+(* 1. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+Notation c1 x := (pair' x).
+Check pair' 0 0 0 : prod' bool bool.
+Check (pair' 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
+Check c1 0 0 0 : prod' bool bool.
+Check fun x : prod' bool bool => match x with c1 0 y 0 => 2 | _ => 1 end.
+
+(* 2. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+Notation c2 x := (@pair' _ x).
+Check (@pair' _ 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
+Check c2 0 0 0 : prod' bool bool.
+Check fun A (x : prod' bool A) => match x with c2 0 y 0 => 2 | _ => 1 end.
+Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ => 1 end.
+
+(* 3. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+Notation c3 x := ((@pair') _ x).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *)
+Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *)
+Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *)
+Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end.
+
+(* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
+(* unless an atomic @ is given *)
+Notation c4 := (@pair').
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "# x" := (pair' x) (at level 0, x at level 1).
+Check pair' 0 0 0 : prod' bool bool.
+Check # 0 _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
+
+(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
+Check ## 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "###" := (@pair') (at level 0).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check ### _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ### _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 8. Notations w/o @ preserves implicit arguments and scopes *)
+Notation "####" := pair' (at level 0).
+Check #### 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
+
+(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *)
+Notation "##### x" := (pair' x) (at level 0, x at level 1).
+Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
diff --git a/test-suite/success/PatternsInBinders.v b/test-suite/success/PatternsInBinders.v
new file mode 100644
index 00000000..77710791
--- /dev/null
+++ b/test-suite/success/PatternsInBinders.v
@@ -0,0 +1,67 @@
+(** The purpose of this file is to test functional properties of the
+    destructive patterns used in binders ([fun] and [forall]). *)
+
+
+Definition swap {A B} '((x,y) : A*B) := (y,x).
+
+(** Tests the use of patterns in [fun] and [Definition] *)
+Section TestFun.
+
+  Variables A B : Type.
+
+  Goal forall (x:A) (y:B), swap (x,y) = (y,x).
+  Proof. reflexivity. Qed.
+
+  Goal forall u:A*B, swap (swap u) = u.
+  Proof. destruct u. reflexivity. Qed.
+
+  Goal @swap A B = fun '(x,y) => (y,x).
+  Proof. reflexivity. Qed.
+
+End TestFun.
+
+
+(** Tests the use of patterns in [forall] *)
+Section TestForall.
+
+  Variables A B : Type.
+
+  Goal forall '((x,y) : A*B), swap (x,y) = (y,x).
+  Proof. intros [x y]. reflexivity. Qed.
+
+  Goal forall x0:A, exists '((x,y) : A*A), swap (x,y) = (x,y).
+  Proof.
+    intros x0.
+    exists (x0,x0).
+    reflexivity.
+  Qed.
+
+End TestForall.
+
+
+
+(** Tests the use of patterns in dependent definitions. *)
+
+Section TestDependent.
+
+  Inductive Fin (n:nat) := Z : Fin n.
+
+  Definition F '(n,p) : Type := (Fin n * Fin p)%type.
+
+  Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
+
+End TestDependent.
+
+
+(** Tests with a few other types just to make sure parsing is
+    robust. *)
+Section TestExtra.
+
+  Definition proj_informative {A P} '(exist _ x _ : { x:A | P x }) : A := x.
+
+  Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo.
+
+  Definition foo '(Bar n b tt p) :=
+    if b then n+p else n-p.
+
+End TestExtra.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 11fbf24d..d8f80424 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -831,7 +831,7 @@ Proof.
  intro n.
  apply nat_ind with (P:= fun n => n <> S n).
  discriminate.
- red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
+ red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;auto.
 Qed.
 
 Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
@@ -1075,8 +1075,8 @@ Proof.
  apply vector_double_rect.
  simpl.
  destruct i; discriminate 1.
- destruct i; simpl;auto.
- injection 1; injection 2;intros; subst a; subst b; auto.
+ destruct i; simpl;auto. 
+ injection 1 as ->; injection 1 as ->; auto.
 Qed.
 
  Set Implicit Arguments.
diff --git a/test-suite/success/TacticNotation2.v b/test-suite/success/TacticNotation2.v
new file mode 100644
index 00000000..cb341b8e
--- /dev/null
+++ b/test-suite/success/TacticNotation2.v
@@ -0,0 +1,12 @@
+Tactic Notation "complete" tactic(tac) := tac; fail.
+
+Ltac f0 := complete (intuition idtac).
+(** FIXME: This is badly printed because of bug #3079.
+    At least we check that it does not fail anomalously. *)
+Print Ltac f0.
+
+Ltac f1 := complete f1.
+Print Ltac f1.
+
+Ltac f2 := complete intuition.
+Print Ltac f2.
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index c8a8b862..023cb5f5 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -53,7 +53,7 @@ Abort.
 
 Lemma essai2 : forall x : nat, x = x.
 
-Fail refine (fix f (x : nat) : x = x := _).
+refine (fix f (x : nat) : x = x := _).
 
 Restart.
 
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 30a2a742..6b1f0315 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,117 @@
+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.
+
+Record Equ (A : Type) (R : A -> A -> Prop).
+Definition equiv {A} R (e : Equ A R) := R.
+Record Refl (A : Type) (R : A -> A -> Prop).
+Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
+Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo.
+
+Variable R : nat -> nat -> Prop.
+Lemma bas : Equ nat R.
+Admitted.
+Hint Resolve bas : foo.
+Hint Extern 1 => match goal with |- (_ -> _ -> Prop) => shelve end : foo.
+
+Goal exists R, @Refl nat R.
+  eexists.
+  Set Typeclasses Debug.
+  (* Fail solve [unshelve eauto with foo]. *)
+  Set Typeclasses Debug Verbosity 1.
+  Test Typeclasses Depth.
+  solve [typeclasses eauto with foo].
+Qed.
+
+Set Typeclasses Compatibility "8.5".
+Parameter f : nat -> Prop.
+Parameter g : nat -> nat -> Prop.
+Parameter h : nat -> nat -> nat -> Prop.
+Axiom a : forall x y, g x y -> f x -> f y.
+Axiom b : forall x (y : Empty_set), g (fst (x,y)) x.
+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.
+  Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
+  Unshelve.
+Abort.
+End bt.
 Generalizable All Variables.
 
 Module mon.
@@ -23,8 +137,15 @@ Notation "'return' t" := (unit t).
 Class A `(e: T) := { a := True }.
 Class B `(e_: T) := { e := e_; sg_ass :> A e }.
 
-Goal forall `{B T}, a.
-  intros. exact I.
+(* Set Typeclasses Debug. *)
+(* Set Typeclasses Debug Verbosity 2. *)
+
+Goal forall `{B T}, Prop.
+  intros. apply a.
+Defined.
+
+Goal forall `{B T}, Prop.
+  intros. refine (@a _ _ _).
 Defined.
 
 Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }.
@@ -57,4 +178,65 @@ Section sec.
  let's try to get rid of the intermediate constant foo.
  Surely we can just expand it inline, right? Wrong!: *)
  Check U (fun x => e x) _.
-End sec.
\ No newline at end of file
+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.
+  Class B.
+  Class C.
+
+  Instance: B -> A | 0.
+  Instance: C -> A | 0.
+  Instance: C -> B -> A | 0.
+  Instance: A -> A | 0.
+  
+  Goal C -> A.
+    intros.
+    Set Typeclasses Debug.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    Fail typeclasses eauto 1.
+    typeclasses eauto 2.
+    Undo.
+    Unset Typeclasses Iterative Deepening.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    typeclasses eauto.
+  Qed.
+
+End IterativeDeepening.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 55b666b7..02e043bc 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -543,7 +543,7 @@ Qed.
 Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
   exists x, exists y, X x y.
 Proof.
-intros; eexists; eexists; case H.
+intros; eexists; eexists ?[y]; case H.
 apply (foo ?y).
 Grab Existential Variables.
 exact 0.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index aaa7b3a5..5477c833 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -45,3 +45,92 @@ Proof.
   eexists. Fail progress debug eauto with test2. 
   progress eauto with test.
 Qed.
+
+(** Patterns of Extern have a "matching" semantics.
+    It is not so for apply/exact hints *)
+
+Class B (A : Type).
+Class I. 
+Instance i : I.
+  
+Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
+Class D (f : nat -> nat -> nat).
+Definition ftest (x y : nat) := x + y.
+Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
+  Admitted.
+Module Instnopat.
+  Local Instance: B nat.
+  (* pattern_of_constr -> B nat *)
+  (* exact hint *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+
+  Local Instance: D ftest.
+  Local Hint Resolve flipD | 0 : typeclass_instances.
+  (* pattern: D (flip _) *)
+  Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)  
+  
+End Instnopat.
+
+Module InstnopatApply.
+  Local Instance: I -> B nat.
+  (* pattern_of_constr -> B nat *)
+  (* apply hint  *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+End InstnopatApply.
+  
+Module InstPat.
+  Hint Extern 3 (B nat) => split : typeclass_instances.
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> true *)
+  Check (_ : B nat).
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> false:
+     Because an inductive in the pattern does not match an evar in the goal *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    (* map_existential -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail progress eauto with typeclass_instances.
+    (* map_eauto -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail typeclasses eauto.
+  Abort.
+
+  Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
+  Module withftest.
+    Local Instance: D ftest.
+
+    Check (_ : D _).
+    (* D_instance_0 : D ftest *)
+    Check (_ : D (flip _)).
+    (* ... : D (flip ftest) *)
+  End withftest.
+  Module withoutftest.
+    Hint Extern 0 (D ftest) => split : typeclass_instances.
+    Check (_ : D _).
+    (* ? : D ?, _not_ looping *)
+    Check (_ : D (flip _)).
+    (* ? : D (flip ?), _not_ looping *)
+
+    Check (_ : D (flip ftest)).
+    (* flipD ftest {|  |} : D (flip ftest) *)
+  End withoutftest.
+End InstPat.
diff --git a/test-suite/success/bigQ.v b/test-suite/success/bigQ.v
new file mode 100644
index 00000000..7fd0cf66
--- /dev/null
+++ b/test-suite/success/bigQ.v
@@ -0,0 +1,66 @@
+Require Import BigQ.
+Import List.
+
+Definition pi_4_approx_low' := 
+(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210782171804373210646804613922337450953858508244032293753591878060539465788294318856859293281629951093130167801471787011911886414492513677892193100809508943832528344473873460853362957387889412799458784754514139679847887887544849825173792522272708046699681079289358082661375778523609867456540595586031625044964543428047238934233579184772793670436643502740076366994465457847106782560289782615794595755672643440040123002018908935362541166831619056664637901929131328502017686713274283777724453661234225382109584471950444925886358166551424008707439387934109226545596919797083495958300914344992836193126080289565652575543234385558967555959267746932292860747199382633363026440008828134867747920263181610216905129926037611247017868033961426567047355301676870662406173724238530061264149506666345040372864118731705584795947926329181826992456072045382170981478151356381437136818835196834068650217794381425547036331194595892801393225038235274901050364737353586927051766717037643833477566087835266968086513005761986678747515870298138062157791066648217784877968385924845017637219384732843791052551854695220023477365706464590594542001161575677402761543188277502092362285265847964496740584911576627239093631932307473445797386335961743298553548881544486940399236133577915988716682746485564575640818803540680574730591500432326858763829791848612343662539095316357052823005419355719381626599487868023399182174939253393897549026675976384326749445831606130546375395770778462506203752920470130305293966478109733954117063941901686840180727195741528561335809865193566993349413786715403053579411364371500063193205131503024022217701373077790337150298315820556080596579100618643147698304927957576213733526923182742441048553793831725592624850721293495085399785588171300815789795594858916409701139277050529011775828846362873246196866089783324522718656445008090114701320562608474099248873638488023114015981013142490827777895317580810590743940417298263300561876701828404744082864248409230009391001735746615476377303707782123483770118391136826609366946585715225248587168403619476143657107412319421501162805102723455593551478028055839072686207007765300258935153546418515706362733656094770289090398825190320430416955807878686642673124733998295439657633866090085982598765253268688814792672416195730086607425842181518560588819896560847103627615434844684536463752986969865794019299978956052589825441828842338163389851892617560591840546654410705167593310272272965900821031821380595084783691324416454359888103920904935692840264474003367023256964191100139001239923263691779167792867186165635514824889759796850863175082506408142175595463676408992027105356481220754473245821534527625758942093801142305560662681150069082553674495761075895588095760081401141419460482860852822686860785424514171214889677926763812031823537071721974799922995763666175738785000806081164280471363125324839717808977470218218571800106898347366938927189989988149888641129263448064762730769285877330997355234347773807099829665997515649429224335217107760728789764718885665291038706425454675746218345291274054088843647602239258308472486102933167465443294268551209015027897159307743987020521392788721231001835675584104894174434637260464035122611721657641428625505184886116917149318963070896162119215386541876236027342810162765609201440423207771441367926085768438143507025739041041240810056881304230519058117534418374553879198061289605354335880794397478047346975609179199801003098836622253165101961484972165230151495472006888128587168049198312469715081555662345452800468933420359802645393289853553618279788400476187713990872203669487294118461245455333004125835663010526985716431187034663870796866708678078952110615910196519835267441831874676895301527286826106517027821074816850326548617513767142627360001181210946100011774672126943957522004190414960909074050454565964857276407084991922274068961845339154089866785707764290964299529444616711194034827611771558783466230353209661849406004241580029437779784290315347968833708422223285859451369907260780956405036020581705441364379616715041818815829810906212826084485200785283123265202151252852134381195424724503189247411069117189489985791487434549080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328
+        # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ
+.
+
+Definition pi_4_approx_high' := 
+(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210788409308322071457087096445676662503017187903223859814905546579050729173916234740628466315449085686468204847296426235788544874405450791749423436215032927889914519102361378633666267941326393265376660400091389373564825046526561381561278586121772300141564909333667988204680492088607706214346458601842899721615765319505314310192693665547163360402786722105590252780194994950097926184146718893770363322073641336811404180286358079915338791029818581497746089864894356686643882883410392601500048021013346713450539807687779704798018559373507951388092945938366448668853081682176581336156031434604604833692503597621519809826880683536141897075567053733515342478008373282599947520770191238802249392773327261328133194484586433840861730959791563023761306622956165536481335792721379318928171897265310054788931201902441066997927781894934061720760080768154565282051604447333036111267534150649674590201404453202347064545359869105856798745664471694795576801148562495225166002814304124970965817043547048503388910163287916513427409193998045119986267987892522931703487420953769290650229176116308194977201080691718825944370436642709192983358059711255925052564016519597530235976618244111239816418652282585432539731271068892992142956810775762851238126881225206289553948196520384709574383566733478326330112084307565420647201107231840508040019131253750047046446929758911912155202166566751947087545292626353331520202690130850009389387290465497377022080531269511355734944672010542204118978272180881335465227900174033380001851066811103401787656367819132934758616060307366679580043123632565656840669377840733018248707250548277181001911990237151790533341326223932843775840498222236867608395855700891719880219904948672458645420169533565809609056209006342663841718949396996175294237942265325043426430990062217643279654512512640557763489491751115437780462208361129433667449740743123546232162409802316714286708788831227582498585478334315076725145986771341647015244092760289407649044493584479944044779273447198382196766547779885914425854375158084417582279211000449529495605127376707776277159376010648950025135061284601443461110447113346277147728593420397807946636800365109579479211273476195727270004743568492888900356505584731622538401071221591141889158461271000051210318027818802379539544396973228585821742794928813630781709195703717312953337431290682263448669168179857644544116657440168099166467471736180072984407514757289757495435699300593165669101965987430482600019222913485092771346963058673132443387835726110205958057187517487684058179749952286341120230051432903482992282688283815697442898155194928723360957436110770317998431272108100149791425689283090777721270428030993332057319821685391144252815655146410678839177846108260765981523812232294638190350688210999605869296307711846463311346627138400477211801219366400312514793356564308532012682051019030257269068628100171220662165246389309014292764479226570049772046255291379151017129899157296574099437276707879597755725339406865738613810979022640265737120949077721294633786520294559343155148383011293584240192753971366644780434237846862975993387453786681995831719537733846579480995517357440575781962659282856696638992709756358478461648462532279323701121386551383509193782388241965285971965887701816406255233933761008649762854363984142178331798953040874526844255758512982810004271235810681505829473926495256537353108899526434200682024946218302499640511518360332022463196599199779172637638655415918976955930735312156870786600023896830267884391447789311101069654521354446521135407720085038662159974712373018912537116964809382149581004863115431780452188813210275393919111435118030412595133958954313836191108258769640843644195537185904547405641078708492098917460393911427237155683288565433183738513871595286090814836422982384810033331519971102974091067660369548406192526284519976668985518575216481570167748402860759832933071281814538397923687510782620605409323050353840034866296214149657376249634795555007199540807313397329050410326609108411299737760271566308288500400587417017113933243099961248847368789383209110747378488312550109911605079801570534271874115018095746872468910162721975463388518648962869080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328
+        # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ
+.
+
+Fixpoint numden_Rcontfrac_tailrecB (accu: list bigZ) (n1 d1: bigZ) (n2 d2: bigZ) (fuel: nat) {struct fuel}:
+  (list bigZ * bigQ * bigQ) :=
+  let default := (rev_append accu nil, BigQ.div (BigQ.Qz n1) (BigQ.Qz d1), BigQ.div (BigQ.Qz n2) (BigQ.Qz d2)) in
+  match fuel with
+  | O => default
+  | S fuel' =>
+    let '(q1, r1) := BigZ.div_eucl n1 d1 in
+    let '(q2, r2) := BigZ.div_eucl n2 d2 in
+    match BigZ.eqb q1 q2 with
+    | false => default
+    | true =>
+      let r1_is_zero := BigZ.eqb r1 0 in
+      let r2_is_zero := BigZ.eqb r2 0 in
+      match Bool.eqb r1_is_zero r2_is_zero with
+      | false => default
+      | true =>
+        match r1_is_zero with
+          | true =>
+            match BigZ.eqb q1 1 with
+              | true => (rev_append accu nil, 1%bigQ, 1%bigQ)
+              | false => (rev_append ((q1 - 1)%bigZ :: accu) nil, 1%bigQ, 1%bigQ)
+            end
+          | false => numden_Rcontfrac_tailrecB (q1 :: accu) d1 r1 d2 r2 fuel'
+        end
+      end
+    end
+  end.
+
+Definition Bnum b :=
+  match b with
+  | BigQ.Qz t => t
+  | BigQ.Qq n d =>
+    if (d =? BigN.zero)%bigN then 0%bigZ else n
+  end.
+
+Definition Bden b :=
+  match b with
+  | BigQ.Qz _ => 1%bigN
+  | BigQ.Qq _ d => if (d =? BigN.zero)%bigN then 1%bigN else d 
+  end.
+
+Definition rat_Rcontfrac_tailrecB q1 q2 :=
+  numden_Rcontfrac_tailrecB nil (Bnum q1) (BigZ.Pos (Bden q1)) (Bnum q2) (BigZ.Pos (Bden q2)).
+
+Definition pi_4_contfrac :=
+  rat_Rcontfrac_tailrecB pi_4_approx_low' pi_4_approx_high' 3000.
+
+(* The following used to fail because of a non canonical representation of 0 in
+the bytecode interpreter. Bug reported privately by Tahina Ramananandro. *)
+Goal pi_4_contfrac = pi_4_contfrac.
+vm_compute.
+reflexivity.
+Qed.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
new file mode 100644
index 00000000..3178c6fc
--- /dev/null
+++ b/test-suite/success/bteauto.v
@@ -0,0 +1,170 @@
+Require Import Program.Tactics.
+Module Backtracking.
+  Class A := { foo : nat }.
+
+  Instance A_1 : A | 2 := { foo := 42 }.
+  Instance A_0 : A | 1 := { foo := 0 }.
+  Lemma aeq (a : A) : foo = foo.
+    reflexivity.
+  Qed.
+  
+  Arguments foo A : clear implicits.
+  Example find42 : exists n, n = 42.
+  Proof.
+    eexists.
+    eapply eq_trans.
+    evar (a : A). subst a.
+    refine (@aeq ?a).
+    Unshelve. all:cycle 1.
+    typeclasses eauto.
+    Fail reflexivity. 
+    Undo 2.
+    (* Without multiple successes it fails *)
+    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 .. ].
+    Undo 1.
+    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
+    Show Proof.  
+  Qed.
+
+  Print find42.
+  
+  Hint Extern 0 (_ = _) => reflexivity : equality.
+  
+  Goal exists n, n = 42.
+    eexists.
+    eapply eq_trans.
+    evar (a : A). subst a.
+    refine (@aeq ?a).
+    Unshelve. all:cycle 1.
+    typeclasses eauto.
+    Fail reflexivity.
+    Undo 2.
+    
+    (* Does backtrack between individual goals *)
+    Set Typeclasses Debug.
+    all:(typeclasses eauto with typeclass_instances equality).
+  Qed.
+  
+  Unset Typeclasses Debug.
+
+  Module Leivant.
+    Axiom A : Type.
+    Existing Class A.
+    Axioms a b c d e: A.
+    
+    Ltac get_value H := eval cbv delta [H] in H.
+    
+    Goal True.
+      Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail.
+    Admitted.
+
+    Goal exists x:A, x=a.
+      unshelve evar (t : A). all:cycle 1.
+      refine (@ex_intro _ _ t _).
+      all:cycle 1.
+      all:(typeclasses eauto + reflexivity).
+    Qed.      
+  End Leivant.
+End Backtracking.
+
+
+Hint Resolve 100 eq_sym eq_trans : core.
+Hint Cut [(_)* eq_sym eq_sym] : core.
+Hint Cut [_* eq_trans eq_trans] : core.
+Hint Cut [_* eq_trans eq_sym eq_trans] : core.
+
+
+Goal forall x y z : nat, x = y -> z = y -> x = z.
+Proof.
+  intros.
+  typeclasses eauto with core.
+Qed.
+
+Module Hierarchies.
+  Class A := mkA { data : nat }.
+  Class B := mkB { aofb :> A }.
+
+  Existing Instance mkB.
+
+  Definition makeB (a : A) : B := _.
+  Definition makeA (a : B) : A := _.
+
+  Fail Timeout 1 Definition makeA' : A := _.
+
+  Hint Cut [_* mkB aofb] : typeclass_instances.
+  Fail Definition makeA' : A := _.
+  Fail Definition makeB' : B := _.
+End Hierarchies.
+
+(** Hint modes *)
+
+Class Equality (A : Type) := { eqp : A -> A -> Prop }.
+
+Check (eqp 0%nat 0).
+
+Instance nat_equality : Equality nat := { eqp := eq }.
+
+Instance default_equality A : Equality A | 1000 :=
+  { eqp := eq }.
+
+Check (eqp 0%nat 0).
+
+(* Defaulting *)
+Check (fun x y => eqp x y).
+(* No more defaulting, reduce "trigger-happiness" *)
+Definition ambiguous x y := eqp x y.
+
+Hint Mode Equality ! : typeclass_instances.
+Fail Definition ambiguous' x y := eqp x y.
+Definition nonambiguous (x y : nat) := eqp x y.
+
+(** Typical looping instances with defaulting: *)
+Definition flip {A B C} (f : A -> B -> C) := fun x y => f y x.
+
+Class SomeProp {A : Type} (f : A -> A -> A) :=
+  { prf : forall x y, f x y = f x y }.
+
+Instance propflip (A : Type) (f : A -> A -> A) :
+  SomeProp f -> SomeProp (flip f).
+Proof.
+  intros []. constructor. reflexivity.
+Qed.
+
+Fail Timeout 1 Check prf.
+
+Hint Mode SomeProp + + : typeclass_instances.
+Check prf.
+Check (fun H : SomeProp plus => _ : SomeProp (flip plus)).
+
+(** Iterative deepening / breadth-first search *)
+
+Module IterativeDeepening.
+
+  Class A.
+  Class B.
+  Class C.
+
+  Instance: B -> A | 0.
+  Instance: C -> A | 0.
+  Instance: C -> B -> A | 0.
+  Instance: A -> A | 0.
+  
+  Goal C -> A.
+    intros.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    Fail typeclasses eauto 1.
+    typeclasses eauto 2.
+    Undo.
+    Unset Typeclasses Iterative Deepening.
+    Fail Timeout 1 typeclasses eauto.
+    Set Typeclasses Iterative Deepening.
+    Typeclasses eauto := debug 3.
+    typeclasses eauto.
+  Qed.
+
+End IterativeDeepening.
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index a70d9196..bbfe5ec4 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -129,5 +129,25 @@ Qed.
 
 End bug_2447.
 
+(* congruence was supposed to do discriminate but it was bugged for
+   types with indices *)
 
+Inductive I : nat -> Type := C : I 0 | D : I 0.
+Goal ~C=D.
+congruence.
+Qed.
+
+(* Example by Jonathan Leivant, congruence up to universes *)
+Section JLeivant.
+  Variables S1 S2 : Set.
+
+  Definition T1 : Type := S1.
+  Definition T2 : Type := S2.
 
+  Goal T1 = T1.
+    congruence.
+    Undo.
+    unfold T1.
+    congruence.
+  Qed.
+End JLeivant.
diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v
index 976bec73..e25510cf 100644
--- a/test-suite/success/clear.v
+++ b/test-suite/success/clear.v
@@ -13,3 +13,21 @@ Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True.
   reflexivity.
 Qed.
 
+Class A.
+
+Section Foo.
+
+  Variable a : A.
+
+  Goal A.
+    solve [typeclasses eauto].
+    Undo 1.
+    clear a.
+    try typeclasses eauto.
+    assert(a:=Build_A).
+    solve [ typeclasses eauto ].
+    Undo 2.
+    assert(b:=Build_A).
+    solve [ typeclasses eauto ].
+  Qed.
+End Foo.
\ No newline at end of file
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
index 4e0b7bf5..5b9265b6 100644
--- a/test-suite/success/coindprim.v
+++ b/test-suite/success/coindprim.v
@@ -1,36 +1,75 @@
+Require Import Program.
+
 Set Primitive Projections.
 
-CoInductive stream A := { hd : A; tl : stream A }.
+CoInductive Stream (A : Type) := mkStream { hd : A; tl : Stream A}.
 
-CoFixpoint ticks : stream unit :=
-  {| hd := tt; tl := ticks |}.
+Arguments mkStream [A] hd tl.
+Arguments hd [A] s.
+Arguments tl [A] s.
 
-Arguments hd [ A ] s.
-Arguments tl [ A ] s.
+Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}.
 
-CoInductive bisim {A} : stream A -> stream A -> Prop :=
-  | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'.
+CoFixpoint ones := {| hd := 1; tl := ones |}.
+CoFixpoint ticks := {| hd := tt; tl := ticks |}.
 
-Lemma bisim_refl {A} (s : stream A) : bisim s s.
-Proof.
-  revert s.
-  cofix aux. intros. constructor. reflexivity. apply aux.
-Defined.
+CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop :=
+  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }.
+Arguments stream_equiv {A} s s'.
 
-Lemma constr : forall (A : Type) (s : stream A),
-    bisim s (Build_stream _ s.(hd) s.(tl)).
-Proof.
-  intros. constructor. reflexivity. simpl. apply bisim_refl.
-Defined.
+Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) :=
+  {| hdeq := eq_refl; tleq := ones_eq |}.
+
+CoFixpoint stream_equiv_refl {A} (s : Stream A) : stream_equiv s s :=
+  {| hdeq := eq_refl; tleq := stream_equiv_refl (tl s) |}.
+
+CoFixpoint stream_equiv_sym {A} (s s' : Stream A) (H : stream_equiv s s') : stream_equiv s' s :=
+  {| hdeq := eq_sym H.(hdeq); tleq := stream_equiv_sym _ _ H.(tleq) |}.
+
+CoFixpoint stream_equiv_trans {A} {s s' s'' : Stream A}
+           (H : stream_equiv s s') (H' : stream_equiv s' s'') : stream_equiv s s'' :=
+  {| hdeq := eq_trans H.(hdeq) H'.(hdeq);
+     tleq := stream_equiv_trans H.(tleq) H'.(tleq) |}.
 
-Lemma constr' : forall (A : Type) (s : stream A),
-  s = Build_stream _ s.(hd) s.(tl).
+Program Definition eta_eq {A} (s : Stream A) : stream_equiv s (eta s):=
+  {| hdeq := eq_refl; tleq := stream_equiv_refl (tl (eta s))|}.
+
+Section Parks.
+  Variable A : Type.
+
+  Variable R : Stream A -> Stream A -> Prop.
+  Hypothesis bisim1 : forall s1 s2:Stream A,
+      R s1 s2 -> hd s1 = hd s2.
+  Hypothesis bisim2 : forall s1 s2:Stream A,
+      R s1 s2 -> R (tl s1) (tl s2).
+  CoFixpoint park_ppl :
+    forall s1 s2:Stream A, R s1 s2 -> stream_equiv s1 s2 :=
+    fun s1 s2 (p : R s1 s2) =>
+      mkStreamEq _ _ _ (bisim1 s1 s2 p)
+      (park_ppl (tl s1)
+                (tl s2)
+                (bisim2 s1 s2 p)).
+End Parks.
+
+Program CoFixpoint iterate {A} (f : A -> A) (x : A) : Stream A :=
+  {| hd := x; tl := iterate f (f x) |}.
+
+Program CoFixpoint map {A B} (f : A -> B) (s : Stream A) : Stream B :=
+  {| hd := f s.(hd); tl := map f s.(tl) |}.
+
+Theorem map_iterate A (f : A -> A) (x : A) : stream_equiv (iterate f (f x))
+                                                         (map f (iterate f x)).
 Proof.
-  intros. 
-  Fail destruct s. 
-Abort.
+apply park_ppl with
+(R:= fun s1 s2 => exists x : A, s1 = iterate f (f x) /\
+                        s2 = map f (iterate f x)).
+now intros s1 s2 (x0,(->,->)).
+intros s1 s2 (x0,(->,->)).
+now exists (f x0).
+now exists x. 
+Qed.
 
-Eval compute in constr _ ticks.
+Fail Check (fun A (s : Stream A) => eq_refl : s = eta s).
 
 Notation convertible x y := (eq_refl x : x = y).
 
diff --git a/test-suite/success/contradiction.v b/test-suite/success/contradiction.v
new file mode 100644
index 00000000..92a7c6cc
--- /dev/null
+++ b/test-suite/success/contradiction.v
@@ -0,0 +1,32 @@
+(* Some tests for contradiction *)
+
+Lemma L1 : forall A B : Prop, A -> ~A -> B.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L2 : forall A B : Prop, ~A -> A -> B.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L3 : forall A : Prop, ~True -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L4 : forall A : Prop, forall x : nat, ~x=x -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L5 : forall A : Prop, forall x y : nat, ~x=y -> x=y -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L6 : forall A : Prop, forall x y : nat, x=y -> ~x=y -> A.
+Proof.
+intros; contradiction.
+Qed.
+
diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v
new file mode 100644
index 00000000..46174e48
--- /dev/null
+++ b/test-suite/success/decl_mode2.v
@@ -0,0 +1,249 @@
+Theorem this_is_trivial: True.
+proof.
+  thus thesis.
+end proof.
+Qed.
+
+Theorem T: (True /\ True) /\ True.
+  split. split.
+proof. (* first subgoal *)
+  thus thesis.
+end proof.
+trivial. (* second subgoal *)
+proof. (* third subgoal *)
+  thus thesis.
+end proof.
+Abort.
+
+Theorem this_is_not_so_trivial: False.
+proof.
+end proof. (* here a warning is issued *)
+Fail Qed. (* fails: the proof in incomplete *)
+Admitted. (* Oops! *)
+
+Theorem T: True.
+proof.
+escape.
+auto.
+return.
+Abort.
+
+Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False).
+intros a b.
+proof.
+assume H:(if a then True else False).
+reconsider H as False.
+reconsider thesis as True.
+Abort.
+
+Theorem T: forall x, x=2 -> 2+x=4.
+proof.
+let x be such that H:(x=2).
+have H':(2+x=2+2) by H.
+Abort.
+
+Theorem T: forall x, x=2 -> 2+x=4.
+proof.
+let x be such that H:(x=2).
+then (2+x=2+2).
+Abort.
+
+Theorem T: forall x, x=2 -> x + x = x * x.
+proof.
+let x be such that H:(x=2).
+have (4 = 4).
+        ~= (2 * 2).
+        ~= (x * x) by H.
+        =~ (2 + 2).
+        =~ H':(x + x) by H.
+Abort.
+
+Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2.
+proof.
+let x be such that H:(x + x = x * x).
+claim H':((x - 2) * x = 0).
+thus thesis. 
+end claim.
+Abort.
+
+Theorem T: forall (A B:Prop), A -> B -> A /\ B.
+intros A B HA HB.
+proof.
+hence B.
+Abort.
+
+Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C.
+intros A B C HA HB HC.
+proof.
+thus B by HB.
+Abort.
+
+Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B.
+intros A B C HA HB HC.
+proof.
+Fail hence C. (* fails *)
+Abort.
+
+Theorem T: forall (A B:Prop), B -> A \/ B.
+intros A B HB.
+proof.
+hence B.
+Abort.
+
+Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D).
+intros A B C D HC HD.
+proof.
+thus C by HC.
+Abort.
+
+Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
+intros P HP.
+proof.
+take 2.
+Abort.
+
+Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x.
+intros P HP.
+proof.
+hence (P 2).
+Abort.
+
+Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y.
+intros P R HP HR.
+proof.
+thus (P 2) by HP.
+Abort.
+
+Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B.
+intros A B P HP HA.
+proof.
+suffices to have x such that HP':(P x) to show B by HP,HP'.
+Abort.
+
+Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x).
+intros A P HP HA.
+proof.
+(* BUG: the next line fails when it should succeed.
+Waiting for someone to investigate the bug.
+focus on (forall x, x = 2 -> P x).
+let x be such that (x = 2).
+hence thesis by HP.
+end focus.
+*)
+Abort.
+
+Theorem T: forall x, x = 0 -> x + x = x * x.
+proof.
+let x be such that H:(x = 0).
+define sqr x as (x * x).
+reconsider thesis as (x + x = sqr x).
+Abort.
+
+Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
+proof.
+let P:(nat -> Prop).
+let x:nat.
+assume HP:(P x).
+Abort.
+
+Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
+proof.
+let P:(nat -> Prop).
+Fail let x. (* fails because x's type is not clear *) 
+let x be such that HP:(P x). (* here x's type is inferred from (P x) *)
+Abort.
+
+Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x.
+proof.
+let P:(nat -> Prop).
+let x:nat.
+assume (P x). (* temporary name created *)
+Abort.
+
+Theorem T: forall (P:nat -> Prop), forall x, P x -> P x.
+proof.
+let P:(nat -> Prop).
+let x be such that (P x). (* temporary name created *)
+Abort.
+
+Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A.
+proof.
+let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A).
+consider x such that HP:(P x) and HA:A from H.
+Abort.
+
+(* Here is an example with pairs: *)
+
+Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p).
+proof.
+let p:(nat * nat)%type.
+consider x:nat,y:nat from p.
+reconsider thesis as (x >= y \/ x < y). 
+Abort.
+
+Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> 
+(exists m, P m) -> P 0.
+proof.
+let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)).
+given m such that Hm:(P m).  
+Abort.
+
+Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C.
+proof.
+let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C).
+assume HAB:(A \/ B).
+per cases on HAB.
+suppose A.
+  hence thesis by HAC.
+suppose HB:B.
+  thus thesis by HB,HBC.
+end cases.
+Abort.
+
+Section Coq.
+
+Hypothesis EM : forall P:Prop, P \/ ~ P.
+
+Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
+proof.
+let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
+per cases of (A \/ ~A) by EM.
+suppose (~A).
+  hence thesis by HNAC.
+suppose A.
+  hence thesis by HAC.
+end cases.
+Abort.
+
+Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C.
+proof.
+let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C).
+per cases on (EM A).
+suppose (~A).
+Abort.
+End Coq.
+
+Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B.
+proof.
+let A:Prop,B:Prop,x:bool.
+per cases on x.
+suppose it is true.
+  assume A.
+  hence A.
+suppose it is false.
+  assume B.
+  hence B.
+end cases.
+Abort.
+
+Theorem T: forall (n:nat), n + 0 = n.
+proof.
+let n:nat.
+per induction on n.
+suppose it is 0.
+  thus (0 + 0 = 0).
+suppose it is (S m) and H:thesis for m.
+  then (S (m + 0) = S m).
+  thus =~ (S m + 0).
+end induction.
+Abort.
\ No newline at end of file
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 9f091e39..90a60daa 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -96,21 +96,21 @@ Abort.
 (* Check that subterm selection does not solve existing evars *)
 
 Goal exists x, S x = S 0.
-eexists.
+eexists ?[x].
 Show x.  (* Incidentally test Show on a named goal *)
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S 0).
 Abort.
 
 Goal exists x, S 0 = S x.
-eexists.
+eexists ?[x].
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S ?x).
 [x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
 Abort.
 
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
-do 2 eexists.
+eexists ?[n]; eexists ?[p].
 destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
 change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n).
 Abort.
@@ -426,7 +426,7 @@ destruct b eqn:H.
 (* Check natural instantiation behavior when the goal has already an evar *)
 
 Goal exists x, S x = x.
-eexists.
+eexists ?[x].
 destruct (S _).
 change (0 = ?x).
 Abort.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 773dd321..160f2d9d 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -5,6 +5,184 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+
+Class A (A : Type).
+  Instance an: A nat.
+
+Class B (A : Type) (a : A).
+Instance bn0: B nat 0.
+Instance bn1: B nat 1.
+
+Goal A nat.
+Proof.
+  typeclasses eauto.
+Qed.
+
+Goal B nat 2.
+Proof.
+  Fail typeclasses eauto.
+Abort.
+
+Goal exists T : Type, A T.
+Proof.
+  eexists. typeclasses eauto.
+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.
+Defined.
+
+Instance ab: A bool. (* Backtrack on A instance *)
+Goal exists (T : Type) (t : T), A T /\ B T t.
+Proof.
+  eexists. eexists. typeclasses eauto.
+Defined.
+
+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 *)
+Goal exists (T : Type) (t : T), { x : A T & C x t }.
+Proof.
+  eexists. eexists. typeclasses eauto.
+Defined.
+
+Class D T `(a: A T).
+  Instance: D _ an.
+Goal exists (T : Type), { x : A T & D T x }.
+Proof.
+  eexists. typeclasses eauto.
+Defined.
+  
+
+(* Example from Nicolas Magaud on coq-club - Jul 2000 *)
+
+Definition Nat : Set := nat.
+Parameter S' : Nat -> Nat.
+Parameter plus' : Nat -> Nat -> Nat.
+
+Lemma simpl_plus_l_rr1 :
+ (forall n0 : Nat,
+  (forall m p : Nat, plus' n0 m = plus' n0 p -> m = p) ->
+  forall m p : Nat, S' (plus' n0 m) = S' (plus' n0 p) -> m = p) ->
+ forall n : Nat,
+ (forall m p : Nat, plus' n m = plus' n p -> m = p) ->
+ forall m p : Nat, S' (plus' n m) = S' (plus' n p) -> m = p.
+  intros.
+  apply H0. apply f_equal_nat.
+  Time info_eauto.
+  Undo.
+  Set Typeclasses Debug.
+  Set Typeclasses Iterative Deepening.
+  Time typeclasses eauto 6 with nocore. Show Proof.
+  Undo.
+  Time eauto. (* does EApply H *)
+Qed.
+
+(* Example from Nicolas Tabareau on coq-club - Feb 2016. 
+  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).
+Notation "x .2" := (projT2 x) (at level 3).
+
+Parameter myType: Type. 
+
+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 refine (fooTobar _ _).1 : typeclass_instances.
+
+Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
+
+Hint Extern 0 { x : _ & _ } => simple 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.
+  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.
@@ -38,23 +216,6 @@ 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.
-Parameter S' : Nat -> Nat.
-Parameter plus' : Nat -> Nat -> Nat.
-
-Lemma simpl_plus_l_rr1 :
- (forall n0 : Nat,
-  (forall m p : Nat, plus' n0 m = plus' n0 p -> m = p) ->
-  forall m p : Nat, S' (plus' n0 m) = S' (plus' n0 p) -> m = p) ->
- forall n : Nat,
- (forall m p : Nat, plus' n m = plus' n p -> m = p) ->
- forall m p : Nat, S' (plus' n m) = S' (plus' n p) -> m = p.
-intros.
- eauto. (* does EApply H *)
+  intros.
+  eauto with essai.
 Qed.
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 1f6af0dc..724e2998 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -14,6 +14,18 @@ Lemma lem1 : forall x y : T, {x = y} + {x <> y}.
  decide equality.
 Qed.
 
+Lemma lem1' : forall x y : T, x = y \/ x <> y.
+ decide equality.
+Qed.
+
+Lemma lem1'' : forall x y : T, {x <> y} + {x = y}.
+ decide equality.
+Qed.
+
+Lemma lem1''' : forall x y : T, x <> y \/ x = y.
+ decide equality.
+Qed.
+
 Lemma lem2 : forall x y : T, {x = y} + {x <> y}.
 intros x y.
  decide equality.
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
new file mode 100644
index 00000000..86814051
--- /dev/null
+++ b/test-suite/success/goal_selector.v
@@ -0,0 +1,55 @@
+Inductive two : bool -> Prop :=
+| Zero : two false
+| One : two true.
+
+Ltac dup :=
+  let H := fresh in assert (forall (P : Prop), P -> P -> P) as H by (intros; trivial);
+  apply H; clear H.
+
+Lemma transform : two false <-> two true.
+Proof. split; intros _; constructor. Qed.
+
+Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
+Proof.
+  do 2 dup.
+  - repeat split.
+    2, 4-99, 100-3:idtac.
+    2-5:exact One.
+    par:exact Zero.
+  - repeat split.
+    3-6:swap 1 4.
+    1-5:swap 1 5.
+    0-4:exact One.
+    all:exact Zero.
+  - repeat split.
+    1, 3:exact Zero.
+    1, 2, 3, 4: exact One.
+  - repeat split.
+    all:apply transform.
+    2, 4, 6:apply transform.
+    all:apply transform.
+    1-5:apply transform.
+    1-6:exact One.
+Qed.
+
+Goal True -> True.
+Proof.
+  intros y; only 1-2 : repeat idtac.
+  1-1:match goal with y : _ |- _ => let x := y in idtac x end.
+  Fail 1-1:let x := y in idtac x.
+  1:let x := y in idtac x.
+  exact I.
+Qed.
+
+Goal True /\ (True /\ True).
+Proof.
+  dup.
+  - split; only 2: (split; exact I).
+    exact I.
+  - split; only 2: split; exact I.
+Qed.
+
+Goal True -> exists (x : Prop), x.
+Proof.
+  intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
+Qed.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index b8c6bf3f..1ed731f5 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -151,3 +151,46 @@ intros x H1 H.
 induction H.
 change (0 = z -> True) in IHrepr''.
 Abort.
+
+(* Test double induction *)
+
+(* This was failing in 8.5 and before because of a bug in the order of
+   hypotheses *)
+
+Inductive I2 : Type :=
+  C2 : forall x:nat, x=x -> I2.
+Goal forall a b:I2, a = b.
+double induction a b.
+Abort.
+
+(* This was leaving useless hypotheses in 8.5 and before because of
+   the same bug. This is a change of compatibility. *)
+
+Inductive I3 : Prop :=
+  C3 : forall x:nat, x=x -> I3.
+Goal forall a b:I3, a = b.
+double induction a b.
+Fail clear H. (* H should have been erased *)
+Abort.
+
+(* This one had quantification in reverse order in 8.5 and before *)
+(* This is a change of compatibility. *)
+
+Goal forall m n, le m n -> le n m -> n=m.
+intros m n. double induction 1 2.
+3:destruct 1. (* Should be "S m0 <= m0" *)
+Abort.
+
+(* Idem *)
+
+Goal forall m n p q, le m n -> le p q -> n+p=m+q.
+intros *. double induction 1 2.
+3:clear H2. (* H2 should have been erased *)
+Abort.
+
+(* This is unchanged *)
+
+Goal forall m n:nat, n=m.
+double induction m n.
+Abort.
+
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 11156aa0..ee69df97 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -84,3 +84,47 @@ Qed.
 Goal forall x : nat, True.
 intros y%(fun x => x).
 Abort.
+
+(* Fixing a bug in the order of side conditions of a "->" step *)
+
+Goal (True -> 1=0) -> 1=1.
+intros ->.
+- reflexivity.
+- exact I.
+Qed.
+
+Goal forall x, (True -> x=0) -> 0=x.
+intros x ->.
+- reflexivity.
+- exact I.
+Qed.
+
+(* Fixing a bug when destructing a type with let-ins in the constructor *)
+
+Inductive I := C : let x:=1 in x=1 -> I.
+Goal I -> True.
+intros [x H]. (* Was failing in 8.5 *)
+Abort.
+
+(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up
+   to skipping let-ins *)
+
+Goal I -> 1=1.
+intros (H).  (* This skips x *)
+exact H.
+Qed.
+
+Goal I -> 1=1.
+Fail intros (x,H,H').
+Fail intros [|].
+intros (x,H).
+exact H.
+Qed.
+
+Goal Acc le 0 -> True.
+Fail induction 1 as (n,H). (* Induction hypothesis is missing *)
+induction 1 as (n,H,IH).
+exact Logic.I.
+Qed.
+
+
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index 5b0502cf..b88c142b 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -58,4 +58,5 @@ Qed.
 
    Lemma test b : b && true = b.
     Fail rewrite andb_true_l.
-   Admitted.
\ No newline at end of file
+   Admitted.
+   
\ No newline at end of file
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 6c4d4ae9..ce909905 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -15,7 +15,7 @@ Ltac F x := idtac; G x
  with G y := idtac; F y.
 
 (* Check that Match Context keeps a closure *)
-Ltac U := let a := constr:I in
+Ltac U := let a := constr:(I) in
           match goal with
           |  |- _ => apply a
           end.
@@ -75,7 +75,7 @@ Qed.
 
 (* Check context binding *)
 Ltac sym t :=
-  match constr:t with
+  match constr:(t) with
   | context C[(?X1 = ?X2)] => context C [X1 = X2]
   end.
 
@@ -143,7 +143,7 @@ Qed.
 
 Ltac check_binding y := cut ((fun y => y) = S).
 Goal True.
-check_binding ipattern:H.
+check_binding ipattern:(H).
 Abort.
 
 (* Check that variables explicitly parsed as ltac variables are not
@@ -151,7 +151,7 @@ Abort.
 
 Ltac afi tac := intros; tac.
 Goal 1 = 2.
-afi ltac:auto.
+afi ltac:(auto).
 Abort.
 
 (* Tactic Notation avec listes *)
@@ -174,7 +174,7 @@ Abort.
    empty args *)
 
 Goal True.
-match constr:@None with @None => exact I end.
+match constr:(@None) with @None => exact I end.
 Abort.
 
 (* Check second-order pattern unification *)
@@ -218,7 +218,7 @@ Ltac Z1 t := set (x:=t).
 Ltac Z2 t := t.
 Goal True -> True.
 Z1 O.
-Z2 ltac:O.
+Z2 ltac:(O).
 exact I.
 Qed.
 
@@ -302,7 +302,7 @@ Abort.
 (* Check instantiation of binders using ltac names *)
 
 Goal True.
-let x := ipattern:y in assert (forall x y, x = y + 0).
+let x := ipattern:(y) in assert (forall x y, x = y + 0).
 intro.
 destruct y. (* Check that the name is y here *)
 Abort.
diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v
new file mode 100644
index 00000000..d5552695
--- /dev/null
+++ b/test-suite/success/ltacprof.v
@@ -0,0 +1,8 @@
+(** Some LtacProf tests *)
+
+Set Ltac Profiling.
+Ltac multi := (idtac + idtac).
+Goal True.
+  try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *)
+Admitted.
+Show Ltac Profile.
diff --git a/test-suite/success/onlyprinting.v b/test-suite/success/onlyprinting.v
new file mode 100644
index 00000000..91a628d7
--- /dev/null
+++ b/test-suite/success/onlyprinting.v
@@ -0,0 +1,7 @@
+Notation "x ++ y" := (plus x y) (only printing).
+
+Fail Check 0 ++ 0.
+
+Notation "x + y" := (max x y) (only printing).
+
+Check (eq_refl : 42 + 18 = 60).
diff --git a/test-suite/success/par_abstract.v b/test-suite/success/par_abstract.v
new file mode 100644
index 00000000..7f6f9d62
--- /dev/null
+++ b/test-suite/success/par_abstract.v
@@ -0,0 +1,25 @@
+Axiom T : Type.
+
+Lemma foo : True * Type.
+Proof.
+  split.
+  par: abstract (exact I || exact T).
+Defined.
+
+(* Yes, these names are generated hence
+   the test is fragile.  I want to assert
+   that abstract was correctly handled
+   by par: *)
+Check foo_subproof.
+Check foo_subproof0.
+Check (refl_equal _ :
+  foo =
+  pair foo_subproof foo_subproof0).
+
+Lemma bar : True * Type.
+Proof.
+  split.
+  par: (exact I || exact T).
+Defined.
+Check (refl_equal _ :
+  bar = pair I T).
diff --git a/test-suite/success/paralleltac.v b/test-suite/success/paralleltac.v
index 94ff96ef..d25fd32a 100644
--- a/test-suite/success/paralleltac.v
+++ b/test-suite/success/paralleltac.v
@@ -1,3 +1,17 @@
+Lemma test_nofail_like_all1 :
+  True /\ False.
+Proof.
+split.
+all: trivial.
+Admitted.
+
+Lemma test_nofail_like_all2 :
+  True /\ False.
+Proof.
+split.
+par: trivial.
+Admitted.
+
 Fixpoint fib n := match n with
   | O => 1
   | S m => match m with
@@ -19,28 +33,28 @@ Lemma test_old x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T1: linear".
-Time all: solve_P.
+Time all: solve [solve_P].
 Qed.
 
 Lemma test_ok x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T2: parallel".
-Time par: solve_P.
+Time par: solve [solve_P].
 Qed.
 
 Lemma test_fail x : P (S x) /\ P x /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T3: linear failure".
-Fail Time all: solve_P.
-all: apply (P_triv Type).
+Fail Time all: solve solve_P.
+all: solve [apply (P_triv Type)].
 Qed.
 
 Lemma test_fail2 x : P (S x) /\ P x /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T4: parallel failure".
-Fail Time par: solve_P.
-all: apply (P_triv Type).
+Fail Time par: solve [solve_P].
+all: solve [apply (P_triv Type)].
 Qed.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 281d707c..2fa77049 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -35,10 +35,6 @@ Set Implicit Arguments.
 
 Check nat.
 
-(* Inductive X (U:Type) := Foo (k : nat) (x : X U).  *)
-(* Parameter x : X nat. *)
-(* Check x.(k). *)
-
 Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
 
 Parameter x:X nat.
@@ -49,19 +45,11 @@ Inductive Y := { next : option Y }.
 
 Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
-Proof. reflexivity. Defined.
-
-Variable t : Y.
-
-Fixpoint yn (n : nat) (y : Y) : Y := 
-  match n with
-    | 0 => t
-    | S n => {| next := Some (yn n y) |}
-  end.
+Proof. Fail reflexivity. Abort.
 
-Lemma eta_ind'  (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
-Proof. reflexivity. Defined.
+Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }.
 
+Fail Scheme Fdef_rec := Induction for Fdef Sort Prop.
 
 (* 
   Rules for parsing and printing of primitive projections and their eta expansions.
diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v
new file mode 100644
index 00000000..414c572f
--- /dev/null
+++ b/test-suite/success/programequality.v
@@ -0,0 +1,13 @@
+Require Import Program.
+
+Axiom t : nat -> Set.
+
+Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type)
+       (a : t x),
+    P (eq_rect _ _ a _ e) e'.
+Proof.
+  intros.
+  pi_eq_proofs. clear e.
+  destruct e'. simpl.
+  change (P a eq_refl).
+Abort.
\ No newline at end of file
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 0befe054..b26a9ff1 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -14,3 +14,16 @@ let name := fresh "fresh" in
 remember (1 + 2) as x eqn:name.
 rewrite fresh.
 Abort.
+
+(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
+                  
+Module A.
+Axiom N : nat.
+End A.
+Module B.
+Include A.
+End B.
+Goal id A.N = B.N.
+reflexivity.
+Qed.           
+                
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 0465c4b3..1f24ef2a 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -166,3 +166,16 @@ Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort.
 Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
 Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort.
 
+(* This should not raise an anomaly as it did for some time in early 2016 *)
+
+Definition t := nat -> bool.
+Definition h (a b : t) := forall n, a n = b n.
+
+Instance subrelh : subrelation h (Morphisms.pointwise_relation nat eq).
+Proof. intros x y H; assumption. Qed.
+
+Goal forall a b, h a b -> a 0 = b 0.
+intros.
+setoid_rewrite H. (* Fallback on ordinary rewrite without anomaly *)
+reflexivity.
+Qed.
diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v
new file mode 100644
index 00000000..3f6b9cb3
--- /dev/null
+++ b/test-suite/success/shrink_abstract.v
@@ -0,0 +1,13 @@
+Set Shrink Abstract.
+
+Definition foo : forall (n m : nat), bool.
+Proof.
+pose (p := 0).
+intros n.
+pose (q := n).
+intros m.
+pose (r := m).
+abstract (destruct m; [left|right]).
+Defined.
+
+Check (foo_subproof : nat -> bool).
diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v
new file mode 100644
index 00000000..676b9787
--- /dev/null
+++ b/test-suite/success/shrink_obligations.v
@@ -0,0 +1,28 @@
+Require Program.
+
+Obligation Tactic := idtac.
+
+Set Shrink Obligations.
+
+Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit :=
+let bar : {r | n < r} := _ in
+let qux : {r | p < r} := _ in
+let quz : m = n -> True := _ in
+tt.
+Next Obligation.
+intros m p n q.
+exists (S n); constructor.
+Qed.
+Next Obligation.
+intros m p n q.
+exists (S (S m)); constructor.
+Qed.
+Next Obligation.
+intros m p n q ? ? H.
+destruct H.
+constructor.
+Qed.
+
+Check (foo_obligation_1 : forall n, {r | n < r}).
+Check (foo_obligation_2 : forall m, {r | (S m) < r}).
+Check (foo_obligation_3 : forall m n, m = n -> True).
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
index d4191b93..2728672f 100644
--- a/test-suite/success/simpl_tuning.v
+++ b/test-suite/success/simpl_tuning.v
@@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
 Abort. 
 
 Definition volatile := fun x : nat => x.
-Arguments volatile /.
+Arguments volatile / _.
 
 Lemma foo : volatile = volatile.
 simpl.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 3faa1ca4..fba05cd9 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -64,3 +64,11 @@ assert (H:=H I).
 match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
+
+(* Test specialize as *)
+
+Goal (forall x, x=0) -> 1=0.
+intros.
+specialize (H 1) as ->.
+reflexivity.
+Qed.
diff --git a/test-suite/success/ssrpattern.v b/test-suite/success/ssrpattern.v
new file mode 100644
index 00000000..96f0bbac
--- /dev/null
+++ b/test-suite/success/ssrpattern.v
@@ -0,0 +1,22 @@
+Require Import ssrmatching.
+
+(*Set Debug SsrMatching.*)
+
+Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) :=
+  let name := fresh in
+  let def_name := fresh in
+  ssrpattern pat;
+  intro name;
+  pose proof (refl_equal name) as def_name;
+  unfold name at 1 in def_name;
+  t def_name;
+  [ rewrite <- def_name | idtac.. ];
+  clear name def_name.
+
+Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4.
+Proof.
+at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place).
+- reflexivity.
+- trivial.
+- trivial.
+Qed.
diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v
new file mode 100644
index 00000000..25ee81b5
--- /dev/null
+++ b/test-suite/success/subst.v
@@ -0,0 +1,42 @@
+(* Test various subtleties of the "subst" tactics *)
+
+(* Should proceed from left to right (see #4222) *)
+Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y.
+intros.
+subst.
+change (3 = 2) in H1.
+change (3 = 3).
+Abort.
+
+(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *)
+Goal forall x y, x = y -> x = 3 -> x = y.
+intros.
+subst.
+change (3 = 3).
+Abort.
+
+(* Should substitute cycles once, until a recursive equation is obtained *)
+(* (failed in 8.4) *)
+Goal forall x y, x = S y -> y = S x -> x = y.
+intros.
+subst.
+change (y = S (S y)) in H0.
+change (S y = y).
+Abort.
+
+(* A bug revealed by OCaml 4.03 warnings *)
+(* fixes in 4e3d464 and 89ec88f for v8.5, 4e3d4646 and 89ec88f1e for v8.6 *)
+Goal forall y, let x:=0 in y=x -> y=y.
+intros * H;
+(* This worked as expected *)
+subst.
+Fail clear H.
+Abort.
+
+Goal forall y, let x:=0 in x=y -> y=y.
+intros * H;
+(* Before the fix, this unfolded x instead of 
+   substituting y and erasing H *)
+subst.
+Fail clear H.
+Abort.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index e00701fb..269359ae 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,3 +60,20 @@ Qed.
 (* Submitted by Danko Ilik (bug report #1507); related to LetIn *)
 
 Record U : Type := { A:=Type; a:A }.
+
+(** Check assignement of sorts to inductives and records. *)
+
+Variable sh : list nat.
+
+Definition is_box_in_shape (b :nat * nat) := True.
+Definition myType := Type.
+
+Module Ind.
+Inductive box_in : myType :=
+  myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in.
+End Ind.
+
+Module Rec.
+Record box_in : myType :=
+  BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }.
+End Rec.
\ No newline at end of file
diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v
index 58fa3974..62df96c0 100644
--- a/test-suite/success/vm_univ_poly.v
+++ b/test-suite/success/vm_univ_poly.v
@@ -38,8 +38,8 @@ Definition _4 : sumbool_copy x = x :=
 
 (* Polymorphic Inductive Types *)
 Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} :=
-| PSome : T -> poption@{i} T
-| PNone : poption@{i} T.
+| PSome : T -> poption T
+| PNone : poption T.
 
 Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T :=
   match p with
@@ -49,7 +49,7 @@ Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x
 
 Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} :=
 | pnil
-| pcons : T -> plist@{i} T -> plist@{i} T.
+| pcons : T -> plist T -> plist T.
 
 Arguments pnil {_}.
 Arguments pcons {_} _ _.
@@ -59,7 +59,7 @@ Polymorphic Definition pmap@{i j}
   fix pmap (ls : plist@{i} T) : plist@{j} U :=
     match ls with
     | @pnil _ => @pnil _
-    | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls)
+    | @pcons _ l ls => @pcons@{j} U (f l) (pmap ls)
     end.
 
 Universe Ubool.
@@ -75,7 +75,7 @@ Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) p
 
 Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} :=
 | Empty
-| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T.
+| Branch : plist@{i} (Tree T) -> Tree T.
 
 Polymorphic Definition pfold@{i u}
             {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) :=
@@ -111,7 +111,7 @@ Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i}
 Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} :=
   match n with
   | O => @Empty nat@{i}
-  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n'))
+  | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree n'))
   end.
 
 Eval compute in height (big_tree (S (S (S O)))).
-- 
cgit v1.2.3