From 70ef4b1a2ad19e461ce2b12feb9b029b9c71c023 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 19 Aug 2014 01:46:37 +0200
Subject: Removing a use of tclSENSITIVE in Rewrite.

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

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 0e5a4805b4..f251d69d90 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1509,8 +1509,8 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	match is_hyp, res with
 	| Some id, (undef, Some p, newt) ->
 	    assert_replacing id newt (new_refine (undef, p))
-	| Some id, (undef, None, newt) -> 
-	    Proofview.tclSENSITIVE (Goal.convert_hyp false (id, None, newt))
+	| Some id, (undef, None, newt) ->
+            Proofview.V82.tactic (Tacmach.convert_hyp_no_check (id, None, newt))
 	| None, (undef, Some p, newt) ->
 	    let refable = Goal.Refinable.make
 	      (fun handle -> 
@@ -1522,7 +1522,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	    in
 	      Proofview.tclSENSITIVE (Goal.bind refable Goal.refine)
 	| None, (undef, None, newt) ->
-	    Proofview.tclSENSITIVE (Goal.convert_concl false newt)
+            Proofview.V82.tactic (Tacmach.convert_concl_no_check newt DEFAULTcast)
   in
   let info =
     bind_gl_info
-- 
cgit v1.2.3