diff options
| author | Pierre-Marie Pédrot | 2018-10-11 18:13:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-15 22:54:37 +0200 |
| commit | 6b5b4db599333546334bcdbd852be72ddb39d9dc (patch) | |
| tree | 5aff3505ee428bff94035d8484d5d1672ac3a78d /plugins/funind | |
| parent | da4c6c4022625b113b7df4a61c93ec351a6d194b (diff) | |
Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.
Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index a2d31780dd..272852d47a 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -48,9 +48,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option PRINTED BY pr_fun_ind_using_typed - RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using - GLOB_TYPED AS constr_with_bindings_opt GLOB_PRINTED BY pr_fun_ind_using | [ "using" constr_with_bindings(c) ] -> [ Some c ] | [ ] -> [ None ] |