Merge branch 'master'.

8 files changed, 359 insertions, 55 deletions

diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 3c696502cd..465b3eb8c0 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -41,6 +41,7 @@ Definition F (x:IND True) (A:Type) :=
 Theorem paradox : False.
   (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *)
 Fail Proof (F C False).
+Abort.
 
 (* Another bug found in November 2015 (a substitution was wrongly
    reversed at pretyping level) *)
@@ -61,3 +62,30 @@ Inductive Ind2 (b:=1) (c:nat) : Type :=
   Constr2 : Ind2 c.
 
 Eval vm_compute in Constr2 2.
+
+(* A bug introduced in ade2363 (similar to #5322 and #5324). This
+   commit started to see that some List.rev was wrong in the "var"
+   case of a pattern-matching problem but it failed to see that a
+   transformation from a list of arguments into a substitution was
+   still needed. *)
+
+(* The order of real arguments was made wrong by ade2363 in the "var"
+   case of the compilation of "match" *)
+
+Inductive IND2 : forall X Y:Type, Type :=
+  CONSTR2 : IND2 unit Empty_set.
+
+Check fun x:IND2 bool nat =>
+  match x in IND2 a b return a with
+  | y => _
+  end = true.
+
+(* From January 2017, using the proper function to turn arguments into
+   a substitution up to a context possibly containing let-ins, so that
+   the following, which was wrong also before ade2363, now works
+   correctly *)
+
+Check fun x:Ind bool nat =>
+  match x in Ind _ X Y Z return Z with
+  | y => (true,0)
+  end.
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index a759674115..6abfca4c3f 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -38,3 +38,10 @@ Abort.
 Goal ~ identity 0 1.
 discriminate.
 Qed.
+
+(* Check discriminate on types with local definitions *)
+
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y, B x true = B y false -> False.
+discriminate.
+Qed.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 89b8bd7ac1..1abe14774c 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -1,4 +1,12 @@
 (* Checks syntax of Hints commands *)
+(* Old-style syntax *)
+Hint Resolve eq_refl eq_sym.
+Hint Resolve eq_refl eq_sym: foo.
+Hint Immediate eq_refl eq_sym.
+Hint Immediate eq_refl eq_sym: foo.
+Hint Unfold fst eq_sym.
+Hint Unfold fst eq_sym: foo.
+
 (* Checks that qualified names are accepted *)
 
 (* New-style syntax *)
@@ -8,13 +16,76 @@ Hint Unfold eq_sym: core.
 Hint Constructors eq: foo bar.
 Hint Extern 3 (_ = _) => apply eq_refl: foo bar.
 
-(* Old-style syntax *)
-Hint Resolve eq_refl eq_sym.
-Hint Resolve eq_refl eq_sym: foo.
-Hint Immediate eq_refl eq_sym.
-Hint Immediate eq_refl eq_sym: foo.
-Hint Unfold fst eq_sym.
-Hint Unfold fst eq_sym: foo.
+(* Extended new syntax with patterns *)
+Hint Resolve eq_refl | 4 (_ = _) : baz.
+Hint Resolve eq_sym eq_trans : baz.
+Hint Extern 3 (_ = _) => apply eq_sym : baz.
+
+Parameter pred : nat -> Prop.
+Parameter pred0 : pred 0.
+Parameter f : nat -> nat.
+Parameter predf : forall n, pred n -> pred (f n).
+
+(* No conversion on let-bound variables and constants in pred (the default) *)
+Hint Resolve pred0 | 1 (pred _) : pred.
+Hint Resolve predf | 0 : pred.
+
+(* Allow full conversion on let-bound variables and constants *)
+Create HintDb predconv discriminated.
+Hint Resolve pred0 | 1 (pred _) : predconv.
+Hint Resolve predf | 0 : predconv.
+
+Goal exists n, pred n.
+  eexists.
+  Fail Timeout 1 typeclasses eauto with pred.
+  Set Typeclasses Filtered Unification.
+  Set Typeclasses Debug Verbosity 2.
+  (* predf is not tried as it doesn't match the goal *)
+  typeclasses eauto with pred.
+Qed.
+
+Parameter predconv : forall n, pred n -> pred (0 + S n).
+
+(* The inferred pattern contains 0 + ?n, syntactic match will fail to see convertible
+ terms *)
+Hint Resolve pred0 : pred2.
+Hint Resolve predconv : pred2.
+
+(** In this database we allow predconv to apply to pred (S _) goals, more generally
+  than the inferred pattern (pred (0 + S _)). *)
+Create HintDb pred2conv discriminated.
+Hint Resolve pred0 : pred2conv.
+Hint Resolve predconv | 1 (pred (S _)) : pred2conv.
+
+Goal pred 3.
+  Fail typeclasses eauto with pred2.
+  typeclasses eauto with pred2conv.
+Abort.
+
+Set Typeclasses Filtered Unification.
+Set Typeclasses Debug Verbosity 2.
+Hint Resolve predconv | 1 (pred _) : pred.
+Hint Resolve predconv | 1 (pred (S _)) : predconv.
+Test Typeclasses Limit Intros.
+Goal pred 3.
+  (* predf is not tried as it doesn't match the goal *)
+  (* predconv is tried but fails as the transparent state doesn't allow
+     unfolding + *)
+  Fail typeclasses eauto with pred.
+  (* Here predconv succeeds as it matches (pred (S _)) and then
+     full unification is allowed *)
+  typeclasses eauto with predconv.
+Qed.
+
+(** The other way around: goal contains redexes instead of instances *)
+Goal exists n, pred (0 + n).
+  eexists.
+  (* predf is applied indefinitely *)
+  Fail Timeout 1 typeclasses eauto with pred.
+  (* pred0 (pred _) matches the goal *)
+  typeclasses eauto with predconv.
+Qed.
+
 
 (* Checks that local names are accepted *)
 Section A.
@@ -105,4 +176,4 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
 
   Timeout 1 Fail apply _. (* 0.06s *)
 Abort.
-End HintCut.
\ No newline at end of file
+End HintCut.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 9661b3bfac..f746def5cb 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 da2183841d..78652fb64b 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -150,6 +150,13 @@ match goal with
 end.
 Abort.
 
+(* Injection in the presence of local definitions *)
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y x' y', B x y = B x' y' -> y = y'.
+intros * [= H1 H2].
+exact H2.
+Qed.
+
 (* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 3eaa04144f..6b1f0315bc 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,79 @@
+Module onlyclasses.
+
+(* In 8.6 we still allow non-class subgoals *)
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Goal Foo * Foo.
+    split. shelve.
+    Set Typeclasses Debug.
+    typeclasses eauto.
+    Unshelve. typeclasses eauto.
+  Qed.
+
+  Module RJung.
+    Class Foo (x : nat).
+      
+      Instance foo x : x = 2 -> Foo x.
+      Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
+      Typeclasses eauto := debug.
+      Check (_ : Foo 2).
+
+
+      Fail Definition foo := (_ : 0 = 0).
+
+  End RJung.
+End onlyclasses.
+
+Module shelve_non_class_subgoals.
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Class Bar := {}.
+  Instance bar1 (f:Foo) : Bar := {}.
+
+  Typeclasses eauto := debug.
+  Set Typeclasses Debug Verbosity 2.
+  Goal Bar.
+    (* Solution has shelved subgoals (of non typeclass type) *)
+    typeclasses eauto.
+  Abort.
+End shelve_non_class_subgoals.
+
+Module RefineVsNoTceauto.
+
+  Class Foo (A : Type) := foo : A.
+  Instance: Foo nat := { foo := 0 }.
+  Instance: Foo nat := { foo := 42 }.
+  Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances.
+  Goal exists (f : Foo nat), @foo _ f = 0.
+  Proof.
+    unshelve (notypeclasses refine (ex_intro _ _ _)). 
+    Set Typeclasses Debug. Set Printing All.
+    all:once (typeclasses eauto).
+    Fail idtac. (* Check no subgoals are left *)
+    Undo 3.
+    (** In this case, the (_ = _) subgoal is not considered 
+        by typeclass resolution *)
+    refine (ex_intro _ _ _). Fail reflexivity.
+  Abort.
+
+End RefineVsNoTceauto.
+
+Module Leivantex2PR339.
+  (** Was a bug preventing to find hints associated with no pattern *)
+  Class Bar := {}.
+  Instance bar1 (t:Type) : Bar.
+  Hint Extern 0 => exact True : typeclass_instances.
+  Typeclasses eauto := debug.
+  Goal Bar.
+    Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto. (* Relies on resolution of a non-class subgoal *)
+    Undo 1.
+    typeclasses eauto with typeclass_instances.
+  Qed.
+End Leivantex2PR339.
+
 Module bt.
 Require Import Equivalence.
 
@@ -22,7 +98,7 @@ Goal exists R, @Refl nat R.
   solve [typeclasses eauto with foo].
 Qed.
 
-(* Set Typeclasses Compatibility "8.5". *)
+Set Typeclasses Compatibility "8.5".
 Parameter f : nat -> Prop.
 Parameter g : nat -> nat -> Prop.
 Parameter h : nat -> nat -> nat -> Prop.
@@ -32,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y.
 Hint Resolve a b c : mybase.
 Goal forall x y z, h x y z -> f x -> f y.
   intros.
-  Set Typeclasses Debug.
-  typeclasses eauto with mybase.
+  Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
   Unshelve.
 Abort.
 End bt.
@@ -62,7 +137,8 @@ Notation "'return' t" := (unit t).
 Class A `(e: T) := { a := True }.
 Class B `(e_: T) := { e := e_; sg_ass :> A e }.
 
-Set Typeclasses Debug.
+(* Set Typeclasses Debug. *)
+(* Set Typeclasses Debug Verbosity 2. *)
 
 Goal forall `{B T}, Prop.
   intros. apply a.
@@ -104,6 +180,40 @@ Section sec.
  Check U (fun x => e x) _.
 End sec.
 
+Module UniqueSolutions.
+  Set Typeclasses Unique Solutions.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := {}.
+    Instance eqb : Eq nat := {}.
+
+    Goal Eq nat.
+      try apply _.
+      Fail exactly_once typeclasses eauto.
+    Abort.
+End UniqueSolutions.
+
+
+Module UniqueInstances.
+  (** Optimize proof search on this class by never backtracking on (closed) goals
+      for it. *)
+  Set Typeclasses Unique Instances.
+  Class Eq (A : Type) : Set.
+    Instance eqa : Eq nat := _. constructor. Qed.
+    Instance eqb : Eq nat := {}.
+    Class Foo (A : Type) (e : Eq A) : Set.
+    Instance fooa : Foo _ eqa := {}.
+
+    Tactic Notation "refineu" open_constr(c) := unshelve refine c.
+
+    Set Typeclasses Debug.
+    Goal { e : Eq nat & Foo nat e }.
+      unshelve refineu (existT _ _ _).
+      all:simpl.
+      (** Does not backtrack on the (wrong) solution eqb *)
+      Fail all:typeclasses eauto.
+    Abort.
+End UniqueInstances.
+
 Module IterativeDeepening.
 
   Class A.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index bb1cf06541..3178c6fc15 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -1,3 +1,4 @@
+Require Import Program.Tactics.
 Module Backtracking.
   Class A := { foo : nat }.
 
@@ -8,7 +9,6 @@ Module Backtracking.
   Qed.
   
   Arguments foo A : clear implicits.
-  
   Example find42 : exists n, n = 42.
   Proof.
     eexists.
@@ -20,9 +20,13 @@ Module Backtracking.
     Fail reflexivity. 
     Undo 2.
     (* Without multiple successes it fails *)
-    Fail all:((once typeclasses eauto) + apply eq_refl).
+    Set Typeclasses Debug Verbosity 2.
+    Fail all:((once (typeclasses eauto with typeclass_instances))
+              + apply eq_refl).
     (* Does backtrack if other goals fail *)
-    all:((typeclasses eauto) + reflexivity).
+    all:[> typeclasses eauto + reflexivity .. ].
+    Undo 1.
+    all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
     Show Proof.  
   Qed.
 
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 4db547f4e4..160f2d9deb 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -5,7 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Require Import List.
 
 Class A (A : Type).
   Instance an: A nat.
@@ -31,6 +30,8 @@ Defined.
 
 Hint Extern 0 (_ /\ _) => constructor : typeclass_instances.
 
+Existing Class and.
+
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
   eexists. eexists. typeclasses eauto.
@@ -46,7 +47,7 @@ Class C {T} `(a : A T) (t : T).
 Require Import Classes.Init.
 Hint Extern 0 { x : ?A & _ } =>
   unshelve class_apply @existT : typeclass_instances.
-
+Existing Class sigT.
 Set Typeclasses Debug.
 Instance can: C an 0.
 (* Backtrack on instance implementation *)
@@ -63,41 +64,6 @@ Proof.
 Defined.
   
 
-Parameter in_list : list (nat * nat) -> nat -> Prop.
-Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
-  ~ in_list l n.
-
-(* Hints Unfold not_in_list. *)
-
-Axiom
-  lem1 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
-
-Axiom
-  lem2 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
-
-Axiom
-  lem3 :
-    forall (l : list (nat * nat)) (n p q : nat),
-    not_in_list ((p, q) :: l) n -> not_in_list l n.
-
-Axiom
-  lem4 :
-    forall (l1 l2 : list (nat * nat)) (n : nat),
-    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
-
-Hint Resolve lem1 lem2 lem3 lem4: essai.
-
-Goal
-forall (l : list (nat * nat)) (n p q : nat),
-not_in_list ((p, q) :: l) n -> not_in_list l n.
-  intros.
-  eauto with essai.
-Qed.
-
 (* Example from Nicolas Magaud on coq-club - Jul 2000 *)
 
 Definition Nat : Set := nat.
@@ -126,6 +92,9 @@ Qed.
   Full backtracking on dependent subgoals.
  *)
 Require Import Coq.Classes.Init.
+
+Module NTabareau.
+
 Set Typeclasses Dependency Order.
 Unset Typeclasses Iterative Deepening.
 Notation "x .1" := (projT1 x) (at level 3).
@@ -149,7 +118,8 @@ Hint Extern 5 (Bar ?D.1) =>
 Hint Extern 5 (Qux ?D.1) =>
     destruct D; simpl : typeclass_instances.
 
-Hint Extern 1 myType => unshelve refine (fooTobar _ _).1 : typeclass_instances.
+Hint Extern 1 myType =>
+  unshelve refine (fooTobar _ _).1 : typeclass_instances.
 
 Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances.
 
@@ -158,8 +128,94 @@ Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instance
 Unset Typeclasses Debug.
 Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
 Proof.
-  Time typeclasses eauto 10.
+  Time typeclasses eauto 10 with typeclass_instances.
   Undo. Set Typeclasses Iterative Deepening.
-  Time typeclasses eauto.
+  Time typeclasses eauto with typeclass_instances.
 Defined.
 
+End NTabareau.
+
+Module NTabareauClasses.
+
+Set Typeclasses Dependency Order.
+Unset Typeclasses Iterative Deepening.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+
+Parameter myType: Type. 
+Existing Class myType.
+
+Class Foo (a:myType) := {}.
+
+Class Bar (a:myType) := {}.
+
+Class Qux (a:myType) := {}.
+
+Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}.
+
+Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}.
+
+Hint Extern 5 (Bar ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 5 (Qux ?D.1) =>
+    destruct D; simpl : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances.
+
+Hint Extern 1 myType =>
+  unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances.
+
+Hint Extern 0 { x : _ & _ } =>
+  unshelve notypeclasses refine (existT _ _ _) : typeclass_instances.
+
+Unset Typeclasses Debug.
+
+Definition trivial a (H : Foo a) : {b : myType & Qux b}. 
+Proof.
+  Time typeclasses eauto 10 with typeclass_instances.
+  Undo. Set Typeclasses Iterative Deepening.
+  (* Much faster in iteratove deepening mode *)
+  Time typeclasses eauto with typeclass_instances.
+Defined.
+
+End NTabareauClasses.
+
+
+Require Import List.
+
+Parameter in_list : list (nat * nat) -> nat -> Prop.
+Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
+  ~ in_list l n.
+
+(* Hints Unfold not_in_list. *)
+
+Axiom
+  lem1 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l1 n.
+
+Axiom
+  lem2 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list (l1 ++ l2) n -> not_in_list l2 n.
+
+Axiom
+  lem3 :
+    forall (l : list (nat * nat)) (n p q : nat),
+    not_in_list ((p, q) :: l) n -> not_in_list l n.
+
+Axiom
+  lem4 :
+    forall (l1 l2 : list (nat * nat)) (n : nat),
+    not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n.
+
+Hint Resolve lem1 lem2 lem3 lem4: essai.
+
+Goal
+forall (l : list (nat * nat)) (n p q : nat),
+not_in_list ((p, q) :: l) n -> not_in_list l n.
+  intros.
+  eauto with essai.
+Qed.