typeclasses eauto Implem/doc of shelving strategy

Now [typeclasses eauto] mimicks what happens during resolution
faithfully, and the shelving behavior/requirements for a successful
proof-search are documented.

3 files changed, 17 insertions, 11 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 4581a7ce40..6885717ec5 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -6,10 +6,10 @@ Module onlyclasses.
   Goal Foo * Foo.
     split. shelve.
     Set Typeclasses Debug.
-    typeclasses eauto.
+    Fail typeclasses eauto.
     typeclasses eauto with typeclass_instances.
     Unshelve. typeclasses eauto with typeclass_instances.
-  Abort.
+  Qed.
 End onlyclasses.
 
 Module shelve_non_class_subgoals.
@@ -22,22 +22,23 @@ Module shelve_non_class_subgoals.
   Typeclasses eauto := debug.
   Set Typeclasses Debug Verbosity 2.
   Goal Bar.
-    (* Solution has shelved subgoals *)
+    (* Solution has shelved subgoals (of non typeclass type) *)
     Fail typeclasses eauto.
   Abort.
 End shelve_non_class_subgoals.
 
-Module shelve_non_class_subgoals2.
+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.
-    debug eauto with typeclass_instances.
-  Qed.  
-End shelve_non_class_subgoals2.
+    Set Typeclasses Debug Verbosity 2.
+    typeclasses eauto with typeclass_instances.
+  Qed.
+End Leivantex2PR339.
 
 Module bt.
 Require Import Equivalence.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index bb1cf06541..f97f764b4d 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -8,7 +8,7 @@ Module Backtracking.
   Qed.
   
   Arguments foo A : clear implicits.
-  
+  Require Import Program.Tactics.
   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 9bcecfe1f3..160f2d9deb 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -176,6 +176,7 @@ 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.