Removing various tactic compatibility layers in core tactics.

3 files changed, 13 insertions, 8 deletions

diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 40f30c794..ff5e7d5ff 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -85,7 +85,7 @@ TACTIC EXTEND not_evar
 END
 
 TACTIC EXTEND is_ground
-  [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
+  [ "is_ground" constr(ty) ] -> [ is_ground ty ]
 END
 
 TACTIC EXTEND autoapply
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c50100bf5..fdcaedab3 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -19,6 +19,7 @@ open Geninterp
 open Extraargs
 open Tacmach
 open Tacticals
+open Proofview.Notations
 open Rewrite
 open Stdarg
 open Pcoq.Vernac_
@@ -123,15 +124,19 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
+  Proofview.Goal.enter { enter = begin fun gl ->
   let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
-    Tacticals.onAllHypsAndConcl
+  let hyps = Tacmach.New.pf_ids_of_hyps gl in
+    Tacticals.New.tclMAP
       (fun cl ->
         match cl with
-          | Some id when is_tac id -> tclIDTAC
-          | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
+          | Some id when is_tac id -> Tacticals.New.tclIDTAC
+          | _ -> cl_rewrite_clause c o AllOccurrences cl)
+      (None :: List.map (fun id -> Some id) hyps)
+  end }
 
 TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
 END
 
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600..12a1566e2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2197,7 +2197,8 @@ let setoid_transitivity c =
     (transitivity_red true c)
     
 let setoid_symmetry_in id =
-  Proofview.V82.tactic (fun gl ->
+  let open Tacmach.New in
+  Proofview.Goal.enter { enter = begin fun gl ->
   let sigma = project gl in
   let ctype = pf_unsafe_type_of gl (mkVar id) in
   let binders,concl = decompose_prod_assum sigma ctype in
@@ -2211,11 +2212,10 @@ let setoid_symmetry_in id =
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
   let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
   let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
-   Proofview.V82.of_tactic
     (tclTHENLAST
       (Tactics.assert_after_replacing id new_hyp)
       (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
-      gl)
+  end }
 
 let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
 let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry