From 29955b2b6e5eb46adc71425956a5c940522fb30d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 29 Apr 2019 20:16:51 +0200
Subject: Deprecating convert_concl_no_check.

---
 plugins/ltac/g_auto.mlg | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index ec5e46d89b..e59076bd63 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -182,9 +182,18 @@ TACTIC EXTEND unify
   }
 END
 
+{
+let deprecated_convert_concl_no_check =
+  CWarnings.create
+    ~name:"convert_concl_no_check" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [convert_concl_no_check] is deprecated. Use [change_no_check] instead.")
+}
 
 TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl ~check:false x DEFAULTcast }
+| ["convert_concl_no_check" constr(x) ] -> {
+    deprecated_convert_concl_no_check ();
+    Tactics.convert_concl ~check:false x DEFAULTcast
+  }
 END
 
 {
-- 
cgit v1.2.3