Implement limited proof search and iterative deepening.

Fix typo in proofview

2 files changed, 33 insertions, 6 deletions

diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index d6e590af30..f25e18acd6 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -23,8 +23,14 @@ 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.
+
+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_ }.
@@ -73,8 +79,15 @@ Module IterativeDeepening.
   Goal C -> A.
     intros.
     Set Typeclasses Debug.
+    Fail Timeout 1 fulleauto.
+    Set Typeclasses Iterative Deepening.
+    Fail fulleauto 1.
+    fulleauto 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/eauto.v b/test-suite/success/eauto.v
index 0fb8cd916a..837d9d4c17 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -52,9 +52,16 @@ Instance can: C an 0.
 (* Backtrack on instance implementation *)
 Goal exists (T : Type) (t : T), { x : A T & C x t }.
 Proof.
-  eexists. eexists.
-  unshelve class_apply @existT; fulleauto.
+  eexists. eexists. fulleauto.
+Defined.
+
+Class D T `(a: A T).
+  Instance: D _ an.
+Goal exists (T : Type), { x : A T & D T x }.
+Proof.
+  eexists. fulleauto.
 Defined.
+  
 
 Parameter in_list : list (nat * nat) -> nat -> Prop.
 Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop :=
@@ -104,6 +111,13 @@ Lemma simpl_plus_l_rr1 :
  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.
+  apply H0. apply f_equal_nat.
+  Time info_eauto.
+  Undo.
+  Unset Typeclasses Debug.
+  Set Typeclasses Iterative Deepening.
+  Time fulleauto 5. Show Proof.
+  Undo.
+  eauto. (* does EApply H *)
 Qed.