Partially porting eauto to the new tactic API.

4 files changed, 27 insertions, 19 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b1cbea51c..5c74d74f8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1309,7 +1309,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
 		      tclFIRST[
 			tclTHEN
 			  (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
-			  e_assumption;
+			  (Proofview.V82.of_tactic e_assumption);
 		      Eauto.eauto_with_bases
 			(true,5)
 			[Evd.empty,Lazy.force refl_equal]
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e97a42e6e..c0fe514f0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -184,7 +184,7 @@ let with_prods nprods poly (c, clenv) f gls =
 
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
-    Eauto.registered_e_assumption ::
+    Proofview.V82.of_tactic Eauto.registered_e_assumption ::
     (tclTHEN (Proofview.V82.of_tactic Tactics.intro)
        (function g'->
 	  let d = pf_last_hyp g' in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 30c5e686a..974181416 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -33,27 +33,35 @@ DECLARE PLUGIN "eauto"
 
 let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
-let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
+let e_give_exact ?(flags=eauto_unif_flags) c =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let t1 = Tacmach.New.pf_type_of gl c in
+  let t2 = Tacmach.New.pf_concl gl in
   if occur_existential t1 || occur_existential t2 then
-     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
-  else Proofview.V82.of_tactic (exact_check c) gl
+     Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (Proofview.V82.tactic (exact_no_check c))
+  else exact_check c
+  end
 
 let assumption id = e_give_exact (mkVar id)
 
-let e_assumption gl =
-  tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
+let e_assumption =
+  Proofview.Goal.enter begin fun gl ->
+    Tacticals.New.tclFIRST (List.map assumption (Tacmach.New.pf_ids_of_hyps gl))
+  end
 
 TACTIC EXTEND eassumption
-| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ]
+| [ "eassumption" ] -> [ e_assumption ]
 END
 
 TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ]
+| [ "eexact" constr(c) ] -> [ e_give_exact c ]
 END
 
-let registered_e_assumption gl =
-  tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl)
-              (pf_ids_of_hyps gl)) gl
+let registered_e_assumption =
+  Proofview.Goal.enter begin fun gl ->
+  Tacticals.New.tclFIRST (List.map (fun id -> e_give_exact (mkVar id))
+              (Tacmach.New.pf_ids_of_hyps gl))
+  end
 
 (************************************************************************)
 (*   PROLOG tactic                                                      *)
@@ -82,7 +90,7 @@ let one_step l gl =
   [Proofview.V82.of_tactic Tactics.intro]
   @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
   @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
-  @ (List.map assumption (pf_ids_of_hyps gl))
+  @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
   if n <= 0 then error "prolog - failure";
@@ -133,7 +141,7 @@ let e_exact poly flags (c,clenv) =
     
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
-    registered_e_assumption ::
+    Proofview.V82.of_tactic registered_e_assumption ::
     (tclTHEN (Proofview.V82.of_tactic Tactics.intro)
        (function g'->
 	  let d = pf_last_hyp g' in
@@ -163,7 +171,7 @@ and e_my_find_search db_list local_db hdc concl =
 	 match t with
 	   | Res_pf (term,cl) -> Proofview.V82.of_tactic (unify_resolve poly st (term,cl))
 	   | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
-	   | Give_exact (c,cl) -> e_exact poly st (c,cl)
+	   | Give_exact (c,cl) -> Proofview.V82.of_tactic (e_exact poly st (c,cl))
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve poly st (term,cl))
 		 (e_trivial_fail_db db_list local_db)
@@ -252,7 +260,7 @@ module SearchProblem = struct
 	let l =
 	  filter_tactics s.tacres
 	    (List.map
-	       (fun id -> (e_give_exact (mkVar id),
+	       (fun id -> (Proofview.V82.of_tactic (e_give_exact (mkVar id)),
 			   lazy (str "exact" ++ spc () ++ pr_id id)))
 	       (pf_ids_of_hyps g))
 	in
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 7073e8a2b..b55c70fa1 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -21,11 +21,11 @@ val wit_auto_using :
     Genarg.genarg_type
 
 
-val e_assumption : tactic
+val e_assumption : unit Proofview.tactic
 
-val registered_e_assumption : tactic
+val registered_e_assumption : unit Proofview.tactic
 
-val e_give_exact : ?flags:Unification.unify_flags -> constr -> tactic
+val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
 
 val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list ->
   hint_db_name list option -> tactic