From 98da9fdce866728f93bc7cb690275f5559aa9bae Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 16 Apr 2017 20:37:15 +0200
Subject: Removing various tactic compatibility layers in core tactics.

---
 plugins/ltac/rewrite.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac/rewrite.ml')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600c..12a1566e20 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
-- 
cgit v1.2.3