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.

---
 tactics/eauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/eauto.ml')

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3019fc0231..70854e6e3c 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -515,6 +515,6 @@ let autounfold_one db cl =
     if did then
       match cl with
       | Some hyp -> change_in_hyp None (make_change_arg c') hyp
-      | None -> convert_concl_no_check c' DEFAULTcast
+      | None -> convert_concl ~check:false c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
-- 
cgit v1.2.3