Putting all the tactics exported by the Tactics module in the new monad API.

4 files changed, 37 insertions, 40 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 8b5f527cd0..ce28eacc09 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -39,15 +39,15 @@ TACTIC EXTEND cut
 END
 
 TACTIC EXTEND exact_no_check
-  [ "exact_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.exact_no_check c) ]
+  [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
 END
 
 TACTIC EXTEND vm_cast_no_check
-  [ "vm_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.vm_cast_no_check c) ]
+  [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
 END
 
 TACTIC EXTEND native_cast_no_check
-  [ "native_cast_no_check" constr(c) ] -> [ Proofview.V82.tactic (Tactics.native_cast_no_check c) ]
+  [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
 END
 
 TACTIC EXTEND casetype
@@ -200,10 +200,10 @@ END
 (** Move *)
 
 TACTIC EXTEND move
-  [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ]
-| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ]
-| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ]
-| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ]
+  [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ]
+| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ]
+| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ]
+| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ]
 END
 
 (** Revert *)
@@ -231,15 +231,15 @@ END
 (* Fix *)
 
 TACTIC EXTEND fix
-  [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ]
-| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ]
+  [ "fix" natural(n) ] -> [ Tactics.fix None n ]
+| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ]
 END
 
 (* Cofix *)
 
 TACTIC EXTEND cofix
-  [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ]
-| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ]
+  [ "cofix" ] -> [ Tactics.cofix None ]
+| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ]
 END
 
 (* Clear *)
@@ -247,7 +247,7 @@ END
 TACTIC EXTEND clear
   [ "clear" hyp_list(ids) ] -> [
     if List.is_empty ids then Tactics.keep []
-    else Proofview.V82.tactic (Tactics.clear ids)
+    else Tactics.clear ids
   ]
 | [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ]
 END
@@ -261,7 +261,7 @@ END
 (* Generalize dependent *)
 
 TACTIC EXTEND generalize_dependent
-  [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ]
+  [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
 END
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 1f3eb13355..451e0987b0 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -582,7 +582,7 @@ END
     during dependent induction. For internal use. *)
 
 TACTIC EXTEND specialize_eqs
-[ "specialize_eqs" hyp(id) ] -> [ Proofview.V82.tactic (specialize_eqs id) ]
+[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ]
 END
 
 (**********************************************************************)
@@ -728,7 +728,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in
        Tacticals.New.tclTHENLIST
-         [Proofview.V82.tactic (Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
+         [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
           Proofview.Goal.nf_enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
             let env = Proofview.Goal.env gl in
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index d650cb5c6f..5d282a6936 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1659,7 +1659,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Trace.name_tactic (fun () -> Pp.str"<exact>") begin
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let (sigma, c_interp) = pf_interp_casted_constr ist gl c in
-        Sigma.Unsafe.of_pair (Proofview.V82.tactic (Tactics.exact_no_check c_interp), sigma)
+        Sigma.Unsafe.of_pair (Tactics.exact_no_check c_interp, sigma)
       end }
       end
   | TacApply (a,ev,cb,cl) ->
@@ -1714,7 +1714,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Proofview.V82.tactic (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0) in
+        let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
@@ -1729,7 +1729,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
-        let tac = Proofview.V82.tactic (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) in
+        let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
@@ -1755,7 +1755,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Tacticals.New.tclWITHHOLES false
         (name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma
+          (Tactics.generalize_gen cl)) sigma
       end }
   | TacLetTac (na,c,clp,b,eqpat) ->
       Proofview.V82.nf_evar_goals <*>
@@ -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/ltac/tauto.ml b/ltac/tauto.ml
index 655bfd5f52..c0cae84c02 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -102,7 +102,7 @@ let assert_ ?by c =
 
 let apply c = Tactics.apply c
 
-let clear id = Proofview.V82.tactic (fun gl -> Tactics.clear [id] gl)
+let clear id = Tactics.clear [id]
 
 let assumption = Tactics.assumption