Purely refactoring and code/API cleanup.

Fix test-suite files

3 files changed, 83 insertions, 16 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 8d6cbfcde..dfa438d90 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -18,6 +18,7 @@ Goal exists R, @Refl nat R.
   Set Typeclasses Debug.
   (* Fail solve [unshelve eauto with foo]. *)
   Set Typeclasses Debug Verbosity 1.
+  Test Typeclasses Depth.
   solve [typeclasses eauto with foo].
 Qed.
 
@@ -117,15 +118,14 @@ Module IterativeDeepening.
   Goal C -> A.
     intros.
     Set Typeclasses Debug.
-    Fail Timeout 1 fulleauto.
+    Fail Timeout 1 typeclasses eauto.
     Set Typeclasses Iterative Deepening.
-    Fail fulleauto 1.
-    fulleauto 2.
+    Fail typeclasses eauto 1.
+    typeclasses eauto 2.
     Undo.
     Unset Typeclasses Iterative Deepening.
     Fail Timeout 1 typeclasses eauto.
     Set Typeclasses Iterative Deepening.
-    Typeclasses eauto := 3.
     typeclasses eauto.
   Qed.
 
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index f55e32032..eadba47b8 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -38,3 +38,69 @@ Goal exists n, n = 42.
   (* Does backtrack between individual goals *)
   all:(typeclasses eauto).
 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.
+    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 := debug 3.
+    typeclasses eauto.
+  Qed.
+
+End IterativeDeepening.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 17b3aaef2..c9c7c611c 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -16,30 +16,30 @@ Instance bn1: B nat 1.
 
 Goal A nat.
 Proof.
-  fulleauto.
+  typeclasses eauto.
 Qed.
 
 Goal B nat 2.
 Proof.
-  Fail fulleauto.
+  Fail typeclasses eauto.
 Abort.
 
 Goal exists T : Type, A T.
 Proof.
-  eexists. fulleauto.
+  eexists. typeclasses eauto.
 Defined.
 
 Hint Extern 0 (_ /\ _) => constructor : typeclass_instances.
 
 Goal exists (T : Type) (t : T), A T /\ B T t.
 Proof.
-  eexists. eexists. fulleauto.
+  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. fulleauto.
+  eexists. eexists. typeclasses eauto.
 Defined.
 
 Class C {T} `(a : A T) (t : T). 
@@ -52,14 +52,14 @@ Instance can: C an 0.
 (* Backtrack on instance implementation *)
 Goal exists (T : Type) (t : T), { x : A T & C x t }.
 Proof.
-  eexists. eexists. fulleauto.
+  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. fulleauto.
+  eexists. typeclasses eauto.
 Defined.
   
 
@@ -115,11 +115,11 @@ Lemma simpl_plus_l_rr1 :
   apply H0. apply f_equal_nat.
   Time info_eauto.
   Undo.
-  Unset Typeclasses Debug.
+  Set Typeclasses Debug.
   Set Typeclasses Iterative Deepening.
-  Time fulleauto 5. Show Proof.
+  Time typeclasses eauto 2 with nocore. Show Proof.
   Undo.
-  eauto. (* does EApply H *)
+  Time eauto. (* does EApply H *)
 Qed.
 
 (* Example from Nicolas Tabareau on coq-club - Feb 2016. 
@@ -155,10 +155,11 @@ 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 fulleauto 10.
+  Time typeclasses eauto 10.
   Undo. Set Typeclasses Iterative Deepening.
-  Time fulleauto.
+  Time typeclasses eauto.
 Defined.