diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index fdeef5f0ac..ff106404c8 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -138,9 +138,7 @@ let warn_deprecated_syntax = ARGUMENT EXTEND firstorder_using TYPED AS reference_list PRINTED BY pr_firstorder_using_typed - RAW_TYPED AS reference_list RAW_PRINTED BY pr_firstorder_using_raw - GLOB_TYPED AS reference_list GLOB_PRINTED BY pr_firstorder_using_glob | [ "using" reference(a) ] -> [ [a] ] | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ] |