diff options
| author | Pierre-Marie Pédrot | 2021-01-22 19:43:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-22 19:43:55 +0100 |
| commit | 5986422fe75d017f75a0223f348d264638c1e33c (patch) | |
| tree | e63232c3924793e1eaedb0192d8ce95cf69d0077 /plugins/ltac | |
| parent | 7d5618684ef17fbb34246f041b3426d42825b85a (diff) | |
| parent | 4fffbe45f42517fbe41fbcf4bf77bfa72fff2579 (diff) | |
Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac')
| -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 |