From d54d63adfd9bd399ca5c31d77977c81887a2e4f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 23 Apr 2019 18:31:45 +0200
Subject: Deprecate the *_no_check variants of conversion tactics.

---
 plugins/ltac/g_auto.mlg | 2 +-
 plugins/ltac/rewrite.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 523c7c8305..ec5e46d89b 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -184,7 +184,7 @@ END
 
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast }
+| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl ~check:false x DEFAULTcast }
 END
 
 {
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d40ba6562..99a9c1ab9a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	    tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
+            convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
             beta_hyp id
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1610,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             end
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_concl_no_check newt DEFAULTcast
+            convert_concl ~check:false newt DEFAULTcast
   in
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-- 
cgit v1.2.3