Rewriting [lapply] tactic in the new monad.

3 files changed, 18 insertions, 16 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 14555279d..ecd7fce31 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1693,12 +1693,11 @@ and interp_atomic ist tac =
         end
       end
   | TacLApply c ->
-      Proofview.V82.tactic begin fun gl -> 
-        let (sigma,c_interp) = pf_interp_constr ist gl c in
-        tclTHEN
-	  (tclEVARS sigma)
+      Proofview.Goal.enter begin fun gl -> 
+        let (sigma,c_interp) = Tacmach.New.of_old (pf_interp_constr ist) gl c in
+        Tacticals.New.tclTHEN
+	  (Proofview.V82.tclEVARS sigma)
 	  (Tactics.cut_and_apply c_interp)
-          gl
       end
 
   (* Context management *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a2bc37dda..151c5b2ce 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -657,9 +657,6 @@ let map_induction_arg f = function
 let apply_type hdcty argl gl =
   refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl
 
-let apply_term hdc argl gl =
-  refine (applist (hdc,argl)) gl
-
 let bring_hyps hyps =
   if List.is_empty hyps then Tacticals.New.tclIDTAC
   else
@@ -1127,14 +1124,21 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars id
   end.
 *)
 
-let cut_and_apply c gl =
-  let goal_constr = pf_concl gl in
-    match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
+let cut_and_apply c =
+  Proofview.Goal.enter begin fun gl ->
+    match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
-	  tclTHENLAST
-	    (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
-	    (apply_term c [mkMeta (new_meta())]) gl
+        let concl = Proofview.Goal.concl gl in
+        let env = Tacmach.New.pf_env gl in
+        Proofview.Refine.refine begin fun h ->
+          let typ = mkProd (Anonymous, c2, concl) in
+          let (h, f) = Proofview.Refine.new_evar h env typ in
+          let (h, x) = Proofview.Refine.new_evar h env c1 in
+          let ans = mkApp (f, [|mkApp (c, [|x|])|]) in
+          (h, ans)
+        end
       | _ -> error "lapply needs a non-dependent product."
+  end
 
 (********************************************************************)
 (*               Exact tactics                                      *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b017b8155..9a2af0835 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -167,7 +167,6 @@ val revert        : Id.t list -> tactic
 (** {6 Resolution tactics. } *)
 
 val apply_type : constr -> constr list -> tactic
-val apply_term : constr -> constr list -> tactic
 val bring_hyps : named_context -> unit Proofview.tactic
 
 val apply                 : constr -> tactic
@@ -179,7 +178,7 @@ val apply_with_bindings_gen :
 val apply_with_bindings   : constr with_bindings -> tactic
 val eapply_with_bindings  : constr with_bindings -> tactic
 
-val cut_and_apply         : constr -> tactic
+val cut_and_apply         : constr -> unit Proofview.tactic
 
 val apply_in :
   advanced_flag -> evars_flag -> Id.t ->