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/ssr | |
| 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/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 989a6c5bf1..d62656f95f 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -491,9 +491,10 @@ let mkhintref ?loc c n = match c.CAst.v with | _ -> mkAppC (c, mkCHoles ?loc n) ARGUMENT EXTEND ssrhintref - PRINTED BY pr_ssrhintref - RAW_TYPED AS constr RAW_PRINTED BY pr_raw_ssrhintref - GLOB_TYPED AS constr GLOB_PRINTED BY pr_glob_ssrhintref + TYPED AS constr + PRINTED BY pr_ssrhintref + RAW_PRINTED BY pr_raw_ssrhintref + GLOB_PRINTED BY pr_glob_ssrhintref | [ constr(c) ] -> [ c ] | [ constr(c) "|" natural(n) ] -> [ mkhintref ~loc c n ] END |