diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 15 |
1 files changed, 0 insertions, 15 deletions
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 @@ -199,20 +198,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 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global |