Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.

5 files changed, 60 insertions, 47 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index c537d895d6..303c73d6bb 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -548,7 +548,10 @@ let unfold_head env (ids, csts) c =
 	in !done_, c'
   in aux c
 
-let autounfold_one db cl gl =
+let autounfold_one db cl =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
   let st =
     List.fold_left (fun (i,c) dbname -> 
       let db = try searchtable_map dbname 
@@ -557,14 +560,15 @@ let autounfold_one db cl gl =
       let (ids, csts) = Hint_db.unfolds db in
 	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
   in
-  let did, c' = unfold_head (pf_env gl) st 
-    (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) 
+  let did, c' = unfold_head env st 
+    (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) 
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp gl
-      | None -> Proofview.V82.of_tactic (convert_concl_no_check c' DEFAULTcast) gl
-    else tclFAIL 0 (str "Nothing to unfold") gl
+      | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp
+      | None -> convert_concl_no_check c' DEFAULTcast
+    else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
+  end
 
 (* 	  Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
 (* 	    (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
@@ -580,9 +584,9 @@ let autounfold_one db cl gl =
       
 TACTIC EXTEND autounfold_one
 | [ "autounfold_one" hintbases(db) "in" hyp(id) ] ->
-    [ Proofview.V82.tactic (autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp))) ]
+    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
 | [ "autounfold_one" hintbases(db) ] ->
-    [ Proofview.V82.tactic (autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None) ]
+    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
       END
 
 TACTIC EXTEND autounfoldify
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d6083860a9..5361125538 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1485,10 +1485,10 @@ let cutSubstInConcl l2r eqn =
   tclTHENFIRST
     (tclTHENLIST [
        (Proofview.Unsafe.tclEVARS sigma);
-       (Proofview.V82.tactic (change_concl typ)); (* Put in pattern form *)
+       (change_concl typ); (* Put in pattern form *)
        (replace_core onConcl l2r eqn)
     ])
-    (Proofview.V82.tactic (change_concl expected)) (* Put in normalized form *)
+    (change_concl expected) (* Put in normalized form *)
    end
 
 let cutSubstInHyp l2r eqn id =
@@ -1500,10 +1500,10 @@ let cutSubstInHyp l2r eqn id =
   tclTHENFIRST
     (tclTHENLIST [
        (Proofview.Unsafe.tclEVARS sigma);
-       (Proofview.V82.tactic (change_in_hyp None (fun s -> s,typ) (id,InHypTypeOnly)));
+       (change_in_hyp None (fun s -> s,typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (Proofview.V82.tactic (change_in_hyp None (fun s -> s,expected) (id,InHypTypeOnly)))
+    (change_in_hyp None (fun s -> s,expected) (id,InHypTypeOnly))
   end
 
 let try_rewrite tac =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 67e924fd6a..289014a58b 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -614,9 +614,11 @@ let out_arg = function
   | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
 
-let hResolve id c occ t gl = 
-  let sigma = project gl in 
-  let env = Termops.clear_named_body id (pf_env gl) in
+let hResolve id c occ t =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
+  let concl = Proofview.Goal.concl gl in
   let env_ids = Termops.ids_of_context env in
   let c_raw = Detyping.detype true env_ids env sigma c in
   let t_raw = Detyping.detype true env_ids env sigma t in
@@ -631,13 +633,15 @@ let hResolve id c occ t gl =
   let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
   let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
-    tclTHEN (Refiner.tclEVARS sigma)
-     (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,pf_concl gl))) gl
+  Tacticals.New.tclTHEN
+    (Proofview.Unsafe.tclEVARS sigma)
+    (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))
+  end
 
-let hResolve_auto id c t gl =
+let hResolve_auto id c t =
   let rec resolve_auto n = 
     try
-      hResolve id c n t gl
+      hResolve id c n t
     with
     | UserError _ as e -> raise e
     | e when Errors.noncritical e -> resolve_auto (n+1)
@@ -645,26 +649,29 @@ let hResolve_auto id c t gl =
   resolve_auto 1
 
 TACTIC EXTEND hresolve_core
-| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ Proofview.V82.tactic (hResolve id c (out_arg occ) t) ]
-| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ Proofview.V82.tactic (hResolve_auto id c t) ]
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c (out_arg occ) t ]
+| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ]
 END
 
 (**
    hget_evar
 *)
 
-let hget_evar n gl =
-  let sigma = project gl in
-  let evl = evar_list (pf_concl gl) in
+let hget_evar n =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let sigma = Proofview.Goal.sigma gl in
+  let concl = Proofview.Goal.concl gl in
+  let evl = evar_list concl in
   if List.length evl < n then
     error "Not enough uninstantiated existential variables.";
   if n <= 0 then error "Incorrect existential variable index.";
   let ev = List.nth evl (n-1) in
   let ev_type = existential_type sigma ev in
-  change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,pf_concl gl)) gl
+  change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
+  end
 
 TACTIC EXTEND hget_evar
-| [ "hget_evar" int_or_var(n) ] -> [ Proofview.V82.tactic (hget_evar (out_arg n)) ]
+| [ "hget_evar" int_or_var(n) ] -> [ hget_evar (out_arg n) ]
 END
 
 (**********************************************************************)
@@ -706,10 +713,8 @@ let  mkCaseEq a  : unit Proofview.tactic =
           Proofview.Goal.nf_enter begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
-            Proofview.V82.tactic begin
-	      change_concl
-	        (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl))
-            end
+	    change_concl
+	      (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl))
           end;
 	  simplest_case a]
   end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8ff4450937..f1c01e7782 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -564,14 +564,17 @@ let e_reduct_option ?(check=false) redfun = function
 (** Versions with evars to maintain the unification of universes resulting
     from conversions. *)
 
-let tclWITHEVARS f k gl =
-  let evm, c' = pf_apply f gl in
-    tclTHEN (tclEVARS evm) (k c') gl
+let tclWITHEVARS f k =
+  Proofview.Goal.enter begin fun gl ->
+  let evm, c' = f gl in
+  Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) (k c')
+  end
 
-let e_change_in_concl (redfun,sty) gl =
+let e_change_in_concl (redfun,sty) =
   tclWITHEVARS
-    (fun env sigma -> redfun env sigma (pf_concl gl))
-    (fun c -> Proofview.V82.of_tactic (convert_concl_no_check c sty)) gl
+    (fun gl -> redfun (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
+        (Proofview.Goal.raw_concl gl))
+    (fun c -> convert_concl_no_check c sty)
 
 let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma =
   match c with
@@ -585,10 +588,12 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
       let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in
 	sigma', (id,Some b',ty')
 
-let e_change_in_hyp redfun (id,where) gl =
+let e_change_in_hyp redfun (id,where) =
   tclWITHEVARS
-    (e_pf_change_decl redfun where (pf_get_hyp gl id))
-    (fun s -> Proofview.V82.of_tactic (convert_hyp s)) gl
+    (fun gl -> e_pf_change_decl redfun where
+      (Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl))
+      (Proofview.Goal.env gl) (Proofview.Goal.sigma gl))
+    convert_hyp
 
 type change_arg = evar_map -> evar_map * constr
 
@@ -654,12 +659,12 @@ let change_option occl t = function
 
 let change chg c cls gl =
   let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
-  tclMAP (function
+  Proofview.V82.of_tactic (Tacticals.New.tclMAP (function
     | OnHyp (id,occs,where) ->
        change_option (bind_change_occurrences occs chg) c (Some (id,where))
     | OnConcl occs ->
        change_option (bind_change_occurrences occs chg) c None)
-    cls gl
+    cls) gl
 
 let change_concl t = 
   change_in_concl None (fun sigma -> sigma, t)
@@ -1122,7 +1127,7 @@ let enforce_prop_bound_names rename tac =
           let env = Proofview.Goal.env gl in
           let sigma = Proofview.Goal.sigma gl in
           let t = Proofview.Goal.concl gl in
-          Proofview.V82.tactic (fun gl -> change_concl (aux env sigma i t) gl)
+          change_concl (aux env sigma i t)
         end in
       (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
         tac
@@ -2755,8 +2760,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
   let rec atomize_one i args avoid =
     if Int.equal i nparams then
       let t = applist (hd, params@args) in
-      Proofview.V82.tactic
-        (change_in_hyp None (fun sigma -> sigma, t) (hyp0,InHypTypeOnly))
+      change_in_hyp None (fun sigma -> sigma, t) (hyp0,InHypTypeOnly)
     else
       let c = List.nth argl (i-1) in
       match kind_of_term c with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c124363a2b..02e3f71603 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -130,10 +130,10 @@ type change_arg = evar_map -> evar_map * constr
 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 change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> tactic
-val change_concl      : constr -> 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 -> tactic
+                        hyp_location -> unit Proofview.tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location -> tactic
 val red_option        : goal_location -> tactic