Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.

1 files changed, 4 insertions, 4 deletions

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 =