diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 11 |
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 { |