From 4fffbe45f42517fbe41fbcf4bf77bfa72fff2579 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 19 Jan 2021 10:34:22 -0800
Subject: Remove convert_concl_no_check

---
 plugins/ltac/g_auto.mlg | 15 ---------------
 1 file changed, 15 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 069a342b2a..82b41e41bd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -11,7 +11,6 @@
 {
 
 open Pp
-open Constr
 open Stdarg
 open Pcoq.Prim
 open Pcoq.Constr
@@ -198,20 +197,6 @@ 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) ] -> {
-    deprecated_convert_concl_no_check ();
-    Tactics.convert_concl ~check:false x DEFAULTcast
-  }
-END
-
 {
 
 let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid
-- 
cgit v1.2.3