diff options
| author | coqbot-app[bot] | 2020-11-10 21:30:52 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-10 21:30:52 +0000 |
| commit | 417e8c513e4372bcd622603912cfb2d9f1069619 (patch) | |
| tree | c999417af80830af45f685751337bf3124652b92 /plugins | |
| parent | fa6c67d721d4178d6b82571feef33c887aef5ba2 (diff) | |
| parent | da9fd81c887024e991467d4dd586661c4ca01022 (diff) | |
Merge PR #13315: Convert logic chapter to prodn
Reviewed-by: Zimmi48
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/g_ground.mlg | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 6ddc6ba21e..d6790d008a 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -108,10 +108,6 @@ let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global -let warn_deprecated_syntax = - CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" - (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator") - } ARGUMENT EXTEND firstorder_using @@ -119,12 +115,7 @@ ARGUMENT EXTEND firstorder_using PRINTED BY { pr_firstorder_using_typed } RAW_PRINTED BY { pr_firstorder_using_raw } GLOB_PRINTED BY { pr_firstorder_using_glob } -| [ "using" reference(a) ] -> { [a] } -| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> { a::l } -| [ "using" reference(a) reference(b) reference_list(l) ] -> { - warn_deprecated_syntax (); - a::b::l - } +| [ "using" ne_reference_list_sep(l,",") ] -> { l } | [ ] -> { [] } END |