Deprecating convert_concl_no_check.

1 files changed, 10 insertions, 1 deletions

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
 
 {