diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-10 10:21:18 -0800 |
| commit | da9fd81c887024e991467d4dd586661c4ca01022 (patch) | |
| tree | 001e9bff33c8d759a8cb79351e2ef36a9839e0c8 /plugins/firstorder | |
| parent | 7d8389d012aa8dbdeb7b82217087f1b7dfb2b24e (diff) | |
Convert logic.rst to prodn
Diffstat (limited to 'plugins/firstorder')
| -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 |