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/ltac/g_auto.ml4 | |
| 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/ltac/g_auto.ml4')
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 35ed14fc18..8eadb66edc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -62,9 +62,7 @@ let pr_auto_using _ _ _ = Pptactic.pr_auto_using ARGUMENT EXTEND auto_using TYPED AS uconstr_list PRINTED BY pr_auto_using - RAW_TYPED AS uconstr_list RAW_PRINTED BY pr_auto_using_raw - GLOB_TYPED AS uconstr_list GLOB_PRINTED BY pr_auto_using_glob | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] | [ ] -> [ [] ] |