Merge remote-tracking branch 'github/pr/339' into v8.6

Was PR#339: Documenting type class options, typeclasses eauto

8 files changed, 377 insertions, 69 deletions

diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index fcdfa0057b..ff515038ec 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -1,4 +1,3 @@
-Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
 Require Coq.Setoids.Setoid.
 Import Coq.Setoids.Setoid.
@@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops.
 Local Existing Instance ILFun_ILogic.
 Definition catOP (P Q: OPred) : OPred := admit.
 Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
-admit.
+apply admit.
 Defined.
 Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
 Class IsPointed (T : Type) := point : T.
@@ -69,8 +68,26 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     pose P;
     refine (P _ _)
   end; unfold Basics.flip.
-  2: solve [ apply reflexivity ].
-  Undo.
-  2: reflexivity. (* Toplevel input, characters 18-29:
-Error:
-Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
+  Focus 2.
+  Set Typeclasses Debug.
+  Set Typeclasses Legacy Resolution.
+  apply reflexivity.
+  (* Debug: 1.1: apply @IsPointed_catOP on
+(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0))
+Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0))
+Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x))
+Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails)
+Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities
+Debug: Backtracking after apply @Equivalence_Reflexive
+Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails)
+Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails)
+Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred)
+*)
+  Undo. Unset Typeclasses Legacy Resolution.
+  Test Typeclasses Unique Solutions.
+  Test Typeclasses Unique Instances.
+  Show Existentials.
+  Set Typeclasses Debug Verbosity 2.
+  Set Printing All.
+  Fail apply reflexivity.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 8dadc2419c..efa4325264 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +46,7 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +109,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +121,7 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    unshelve (refine (pr1 (isconnected_elim _ _))).
-    exact b.
+    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
     intros [a p].
     exact (transport P p (d a)).
   Defined.
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
new file mode 100644
index 0000000000..83d4ed69d4
--- /dev/null
+++ b/test-suite/bugs/closed/4095.v
@@ -0,0 +1,87 @@
+(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Require Import TestSuite.admit.
+Require Import Coq.Setoids.Setoid.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+Local Existing Instance ILFun_Ops.
+Local Existing Instance ILFun_ILogic.
+Definition catOP (P Q: OPred) : OPred := admit.
+Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
+admit.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end.
+  Undo.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
+    set(p:=P)
+  end. (* Toplevel input, characters 15-182:
+Error: Cannot infer an instance of type
+"PointedOPred" for the variable p in environment:
+T : Type
+O0 : T -> OPred
+O1 : T -> PointedOPred
+tr : T -> T
+O2 : PointedOPred
+x0 : T
+H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v
index e884355fde..1e47f2957b 100644
--- a/test-suite/bugs/closed/4863.v
+++ b/test-suite/bugs/closed/4863.v
@@ -3,14 +3,14 @@ Require Import Classes.DecidableClass.
 Inductive Foo : Set :=
 | foo1 | foo2.
 
-Instance Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
+Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P.
 Proof.
   intros P H.
   refine (Build_Decidable _ (if H then true else false) _).
   intuition congruence.
 Qed.
 
-Hint Extern 100 ({?A = ?B}+{~ ?A = ?B}) => abstract (abstract (abstract (decide equality))) : typeclass_instances.
+Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances.
 
 Goal forall (a b : Foo), {a=b}+{a<>b}.
 intros.
@@ -21,7 +21,8 @@ Check ltac:(abstract (exact I)) : True.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.
-split. typeclasses eauto. typeclasses eauto. Qed.
+split. typeclasses eauto. 
+typeclasses eauto. Qed.
 
 Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b).
 intros.
diff --git a/test-suite/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/Typeclasses.v b/test-suite/success/Typeclasses.v
index 3eaa04144f..6885717ec5 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,45 @@
+Module onlyclasses.
+
+  Variable Foo : Type.
+  Variable foo : Foo.
+  Hint Extern 0 Foo => exact foo : typeclass_instances.
+  Goal Foo * Foo.
+    split. shelve.
+    Set Typeclasses Debug.
+    Fail typeclasses eauto.
+    typeclasses eauto with typeclass_instances.
+    Unshelve. typeclasses eauto with typeclass_instances.
+  Qed.
+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) *)
+    Fail typeclasses eauto.
+  Abort.
+End shelve_non_class_subgoals.
+
+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.
+    Fail typeclasses eauto.
+    Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto with typeclass_instances.
+  Qed.
+End Leivantex2PR339.
+
 Module bt.
 Require Import Equivalence.
 
@@ -104,6 +146,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.