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 | |
| 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')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index f4555509cc..0c6d10bf8c 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -285,9 +285,7 @@ let in_clause' = Pltac.in_clause ARGUMENT EXTEND in_clause TYPED AS clause_dft_concl PRINTED BY pr_in_top_clause - RAW_TYPED AS clause_dft_concl RAW_PRINTED BY pr_in_clause - GLOB_TYPED AS clause_dft_concl GLOB_PRINTED BY pr_in_clause | [ in_clause'(cl) ] -> [ cl ] END 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 ] | [ ] -> [ [] ] |