Code factorization of tactic "unfold_body".

3 files changed, 19 insertions, 34 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index c9ecc55d1..b287eb8e5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1608,26 +1608,6 @@ user = raise user error specific to rewrite
 (**********************************************************************)
 (* Substitutions tactics (JCF) *)
 
-let unfold_body x =
-  Proofview.Goal.enter { enter = begin fun gl ->
-  (** We normalize the given hypothesis immediately. *)
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let (_, xval, _) = Context.Named.lookup x hyps in
-  let xval = match xval with
-  | None -> errorlabstrm "unfold_body"
-    (pr_id x ++ str" is not a defined hypothesis.")
-  | Some xval -> pf_nf_evar gl xval
-  in
-  afterHyp x begin fun aft ->
-  let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in
-  let xvar = mkVar x in
-  let rfun _ _ c = replace_term xvar xval c in
-  let reducth h = reduct_in_hyp rfun h in
-  let reductc = reduct_in_concl (rfun, DEFAULTcast) in
-  tclTHENLIST [tclMAP reducth hl; reductc]
-  end
-  end }
-
 let restrict_to_eq_and_identity eq = (* compatibility *)
   if not (is_global glob_eq eq) &&
     not (is_global glob_identity eq) 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 210888b67..e36353847 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2721,23 +2721,28 @@ let specialize (c,lbind) =
 
 (* The two following functions should already exist, but found nowhere *)
 (* Unfolds x by its definition everywhere *)
-let unfold_body x gl =
-  let hyps = pf_hyps gl in
-  let xval =
-    match Context.Named.lookup x hyps with
-        (_,Some xval,_) -> xval
-      | _ -> errorlabstrm "unfold_body"
-          (pr_id x ++ str" is not a defined hypothesis.") in
-  let aft = afterHyp x gl in
+let unfold_body x =
+  Proofview.Goal.enter { enter = begin fun gl ->
+  (** We normalize the given hypothesis immediately. *)
+  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  let (_, xval, _) = Context.Named.lookup x hyps in
+  let xval = match xval with
+  | None -> errorlabstrm "unfold_body"
+    (pr_id x ++ str" is not a defined hypothesis.")
+  | Some xval -> pf_nf_evar gl xval
+  in
+  Tacticals.New.afterHyp x begin fun aft ->
   let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
-  tclTHENLIST
-    [tclMAP (fun h -> Proofview.V82.of_tactic (reduct_in_hyp rfun h)) hl;
-     Proofview.V82.of_tactic (reduct_in_concl (rfun,DEFAULTcast))] gl
+  let reducth h = reduct_in_hyp rfun h in
+  let reductc = reduct_in_concl (rfun, DEFAULTcast) in
+  Tacticals.New.tclTHENLIST [Tacticals.New.tclMAP reducth hl; reductc]
+  end
+  end }
 
 (* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id])
+let expand_hyp id = Tacticals.New.tclTHEN (Tacticals.New.tclTRY (unfold_body id)) (Proofview.V82.tactic (clear [id]))
 
 (*****************************)
 (* High-level induction      *)
@@ -3891,7 +3896,7 @@ let apply_induction_in_context hyp0 inhyps elim indvars names induct_tac =
         if deps = [] then Proofview.tclUNIT () else apply_type tmpcl deps_cstr;
         (* side-conditions in elim (resp case) schemes come last (resp first) *)
         induct_tac elim;
-        Proofview.V82.tactic (tclMAP expand_hyp toclear)
+        Tacticals.New.tclMAP expand_hyp toclear;
       ])
       (Array.map2
          (induct_discharge lhyp0 avoid (re_intro_dependent_hypotheses statuslists))
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 367430d91..26ea01769 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -165,7 +165,7 @@ val unfold_constr     : global_reference -> unit Proofview.tactic
 
 val clear         : Id.t list -> tactic
 val clear_body    : Id.t list -> unit Proofview.tactic
-val unfold_body   : Id.t -> tactic
+val unfold_body   : Id.t -> unit Proofview.tactic
 val keep          : Id.t list -> unit Proofview.tactic
 val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic