Moving conversion functions to the new tactic API.

7 files changed, 39 insertions, 36 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c9b2c7cfd..3ac3daef9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -245,7 +245,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
          Proofview.V82.tactic (tclTHEN
 				 (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags))))
 				 (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
-      | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
+      | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (Proofview.V82.of_tactic (unfold_in_concl [AllOccurrences,c])))
       | Extern tacast -> conclPattern concl p tacast
       in
       let tac = Proofview.V82.of_tactic (run_hint t tac) in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 6117c8b43..ae85f02d5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -503,7 +503,7 @@ let autounfolds db occs cls gl =
     let ids = Idset.filter (fun id -> List.mem id hyps) ids in
       Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
 	(Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
-  in unfold_option unfolds cls gl
+  in Proofview.V82.of_tactic (unfold_option unfolds cls) gl
 
 let autounfold db cls gl =
   let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index be4b13597..7c821ddcb 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -123,7 +123,7 @@ let diseqCase hyps eqonleft =
   (tclTHEN (intro_using diseq)
   (tclTHEN (choose_noteq eqonleft)
   (tclTHEN (rewrite_and_clear (List.rev hyps))
-  (tclTHEN  (Proofview.V82.tactic red_in_concl)
+  (tclTHEN  (red_in_concl)
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (Simple.apply (mkVar diseq))
   (tclTHEN  (Extratactics.injHyp absurd)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1e814e861..c9ecc55d1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1622,8 +1622,8 @@ let unfold_body x =
   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 = Proofview.V82.tactic (fun gl -> reduct_in_hyp rfun h gl) in
-  let reductc = Proofview.V82.tactic (fun gl -> reduct_in_concl (rfun, DEFAULTcast) gl) 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 }
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index d0a090e5c..8b71affff 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1569,10 +1569,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             convert_concl_no_check newt DEFAULTcast
   in
   let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
-  let beta = Proofview.V82.tactic (Tactics.reduct_in_concl (beta_red, DEFAULTcast)) in
+  let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
   let opt_beta = match clause with
   | None -> Proofview.tclUNIT ()
-  | Some id -> Proofview.V82.tactic (Tactics.reduct_in_hyp beta_red (id, InHyp))
+  | Some id -> Tactics.reduct_in_hyp beta_red (id, InHyp)
   in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f76f4f6e2..28d3ed18a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -470,7 +470,7 @@ let cofix ido gl = match ido with
 type tactic_reduction = env -> evar_map -> constr -> constr
 
 let pf_reduce_decl redfun where (id,c,ty) gl =
-  let redfun' = Tacmach.pf_reduce redfun gl in
+  let redfun' = Tacmach.New.pf_apply redfun gl in
   match c with
   | None ->
       if where == InHypValueOnly then
@@ -549,12 +549,15 @@ let bind_red_expr_occurrences occs nbcl redexp =
    reduction function either to the conclusion or to a
    certain hypothesis *)
 
-let reduct_in_concl (redfun,sty) gl =
-  Proofview.V82.of_tactic (convert_concl_no_check (Tacmach.pf_reduce redfun gl (Tacmach.pf_concl gl)) sty) gl
+let reduct_in_concl (redfun,sty) =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+    convert_concl_no_check (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
+  end }
 
-let reduct_in_hyp ?(check=false) redfun (id,where) gl =
-  Proofview.V82.of_tactic (convert_hyp ~check
-    (pf_reduce_decl redfun where (Tacmach.pf_get_hyp gl id) gl)) gl
+let reduct_in_hyp ?(check=false) redfun (id,where) =
+  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl)
+  end }
 
 let revert_cast (redfun,kind as r) =
   if kind == DEFAULTcast then (redfun,REVERTcast) else r
@@ -798,7 +801,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
           else Proofview.tclUNIT ()
         end <*>
 	  Proofview.tclORELSE
-	  (Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
+	  (Tacticals.New.tclTHEN hnf_in_concl
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function (e, info) -> match e with
             | RefinerError IntroNeedsProduct ->
@@ -2728,8 +2731,8 @@ let unfold_body x gl =
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
-    [tclMAP (fun h -> reduct_in_hyp rfun h) hl;
-     reduct_in_concl (rfun,DEFAULTcast)] gl
+    [tclMAP (fun h -> Proofview.V82.of_tactic (reduct_in_hyp rfun h)) hl;
+     Proofview.V82.of_tactic (reduct_in_concl (rfun,DEFAULTcast))] gl
 
 (* Either unfold and clear if defined or simply clear if not a definition *)
 let expand_hyp id = tclTHEN (tclTRY (unfold_body id)) (clear [id])
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5564b61c3..657367e36 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -128,38 +128,38 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 type change_arg = patvar_map -> constr Sigma.run
 
 val make_change_arg   : constr -> change_arg
-val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic
-val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic
-val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
+val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
+val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
+val reduct_in_concl   : tactic_reduction * cast_kind -> unit Proofview.tactic
 val change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
 val change_concl      : constr -> unit Proofview.tactic
 val change_in_hyp     : (occurrences * constr_pattern) option -> change_arg ->
                         hyp_location -> unit Proofview.tactic
-val red_in_concl      : tactic
-val red_in_hyp        : hyp_location -> tactic
-val red_option        : goal_location -> tactic
-val hnf_in_concl      : tactic
-val hnf_in_hyp        : hyp_location -> tactic
-val hnf_option        : goal_location -> tactic
-val simpl_in_concl    : tactic
-val simpl_in_hyp      : hyp_location -> tactic
-val simpl_option      : goal_location -> tactic
-val normalise_in_concl : tactic
-val normalise_in_hyp  : hyp_location -> tactic
-val normalise_option  : goal_location -> tactic
-val normalise_vm_in_concl : tactic
+val red_in_concl      : unit Proofview.tactic
+val red_in_hyp        : hyp_location -> unit Proofview.tactic
+val red_option        : goal_location -> unit Proofview.tactic
+val hnf_in_concl      : unit Proofview.tactic
+val hnf_in_hyp        : hyp_location -> unit Proofview.tactic
+val hnf_option        : goal_location -> unit Proofview.tactic
+val simpl_in_concl    : unit Proofview.tactic
+val simpl_in_hyp      : hyp_location -> unit Proofview.tactic
+val simpl_option      : goal_location -> unit Proofview.tactic
+val normalise_in_concl : unit Proofview.tactic
+val normalise_in_hyp  : hyp_location -> unit Proofview.tactic
+val normalise_option  : goal_location -> unit Proofview.tactic
+val normalise_vm_in_concl : unit Proofview.tactic
 val unfold_in_concl   :
-  (occurrences * evaluable_global_reference) list -> tactic
+  (occurrences * evaluable_global_reference) list -> unit Proofview.tactic
 val unfold_in_hyp     :
-  (occurrences * evaluable_global_reference) list -> hyp_location -> tactic
+  (occurrences * evaluable_global_reference) list -> hyp_location -> unit Proofview.tactic
 val unfold_option     :
-  (occurrences * evaluable_global_reference) list -> goal_location -> tactic
+  (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
 val change            :
   constr_pattern option -> change_arg -> clause -> tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic
-val unfold_constr     : global_reference -> tactic
+val unfold_constr     : global_reference -> unit Proofview.tactic
 
 (** {6 Modification of the local context. } *)