Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.

10 files changed, 70 insertions, 57 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6abf96dcee..57268a9cfa 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -247,7 +247,7 @@ module Btauto = struct
           let fr = reify env fr in
           let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
           Tacticals.New.tclTHENLIST [
-            Proofview.V82.tactic (Tactics.change_concl changed_gl);
+            Tactics.change_concl changed_gl;
             Tactics.apply (Lazy.force soundness);
             Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
             try_unification env
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 551b210d37..4b70201b22 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -588,9 +588,9 @@ let rec fourier () =
                       else tac_zero_infeq_false gl (rational_to_fraction cres)
            in
            tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq))
-                     [Tacticals.New.tclTHEN (Proofview.V82.tactic (change_concl
+                     [Tacticals.New.tclTHEN (change_concl
 			       (mkAppL [| get coq_not; ineq|]
-				       )))
+				       ))
 		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
 					       else get coq_Rnot_le_le))
 			    (Tacticals.New.tclTHENS (Equality.replace
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index fd54584bc8..a38764c5bd 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -673,9 +673,9 @@ let mkDestructEq :
     tclTHENLIST
      [Simple.generalize new_hyps;
       (fun g2 ->
-	change_in_concl None
+	Proofview.V82.of_tactic (change_in_concl None
 	  (fun sigma ->
-	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)) g2);
+	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index db22727fc4..dfeeb49047 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1392,7 +1392,7 @@ let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic =
  (* todo : directly generate the proof term - or generalize befor conversion? *)
  Tacticals.tclTHENSEQ [
   (fun gl -> 
-  Tactics.change_concl
+   Proofview.V82.of_tactic (Tactics.change_concl
    (set
      [
       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
@@ -1401,7 +1401,7 @@ let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic =
 	 [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); 
       ("__wit", cert, cert_typ)
      ]
-     (Tacmach.pf_concl gl)) gl);
+     (Tacmach.pf_concl gl))) gl);
   Tactics.generalize env ;
   Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ; 
  ] 
@@ -1683,7 +1683,7 @@ let micromega_order_changer cert env ff gl =
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
  let vm = dump_varmap (typ) env in
-  Tactics.change_concl
+  Proofview.V82.of_tactic (Tactics.change_concl
    (set
      [
       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
@@ -1693,7 +1693,7 @@ let micromega_order_changer cert env ff gl =
       ("__wit", cert, cert_typ)
      ]
      (Tacmach.pf_concl gl)
-   )
+   ))
    gl
 
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 1835b6cc99..f9219407e9 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1282,7 +1282,7 @@ let resolution env full_reified_goal systems_list =
 
   Tactics.generalize
     (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
-  Tactics.change_concl reified >>
+  Proofview.V82.of_tactic (Tactics.change_concl reified) >>
   Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
   Tactics.normalise_vm_in_concl >>
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