Put the "change" tactic in the monad.

3 files changed, 24 insertions, 25 deletions

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 7ec1b2ca0c..5d282a6936 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1879,7 +1879,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           in
           Sigma.Unsafe.of_pair (c, sigma)
         end } in
-        Proofview.V82.tactic (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl))
+        Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
       end }
       end
   | TacChange (Some op,c,cl) ->
@@ -1889,25 +1889,22 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
-        Proofview.V82.tactic begin fun gl -> 
-          let op = interp_typed_pattern ist env sigma op in
-          let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
-          let c_interp patvars = { Sigma.run = begin fun sigma ->
-	    let lfun' = Id.Map.fold (fun id c lfun ->
-	      Id.Map.add id (Value.of_constr c) lfun) 
-	      patvars ist.lfun
-	    in
-	    let ist = { ist with lfun = lfun' } in
-	      try
-                let sigma = Sigma.to_evar_map sigma in
-                let (sigma, c) = interp_constr ist env sigma c in
-                Sigma.Unsafe.of_pair (c, sigma)
-	      with e when to_catch e (* Hack *) ->
-		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
-          end } in
-	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
-	      gl
-        end
+        let op = interp_typed_pattern ist env sigma op in
+        let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
+        let c_interp patvars = { Sigma.run = begin fun sigma ->
+          let lfun' = Id.Map.fold (fun id c lfun ->
+            Id.Map.add id (Value.of_constr c) lfun) 
+            patvars ist.lfun
+          in
+          let ist = { ist with lfun = lfun' } in
+            try
+              let sigma = Sigma.to_evar_map sigma in
+              let (sigma, c) = interp_constr ist env sigma c in
+              Sigma.Unsafe.of_pair (c, sigma)
+            with e when to_catch e (* Hack *) ->
+              errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+        end } in
+        Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
       end }
       end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59e6a1c82a..83b8aacfea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -825,14 +825,16 @@ let change_option occl t = function
   | Some id -> change_in_hyp occl t id
   | None -> change_in_concl occl t
 
-let change chg c cls gl =
-  let cls = concrete_clause_of (fun () -> Tacmach.pf_ids_of_hyps gl) cls in
-  Proofview.V82.of_tactic (Tacticals.New.tclMAP (function
+let change chg c cls =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let cls = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cls in
+    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
+  end }
 
 let change_concl t = 
   change_in_concl None (make_change_arg t)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6987e5b70e..046a15d148 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -154,7 +154,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> unit Proofview.tactic
 val change            :
-  constr_pattern option -> change_arg -> clause -> tactic
+  constr_pattern option -> change_arg -> clause -> unit Proofview.tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> unit Proofview.tactic
 val reduce            : red_expr -> clause -> unit Proofview.tactic