diff options
| author | Pierre-Marie Pédrot | 2016-04-13 12:00:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-13 12:03:34 +0200 |
| commit | f0f3d650ec4fcd1644811e099f0f3f50d660a992 (patch) | |
| tree | e4a99885401e799e1e578430daf1ab2bb51e5d16 /ltac/extraargs.ml4 | |
| parent | d78784bd86d3d571bb2891356e9e9718c69976ba (diff) | |
| parent | d632f64403da813e240973a9caf06c79e262a7ec (diff) | |
Uniformizing the semantics of ARGUMENT EXTEND macros.
Most notably, we bring the single argument and three argument variants
closer, so that the various TYPED AS clauses may be optional. Compile-time
warnings have been added for redundant clauses.
Diffstat (limited to 'ltac/extraargs.ml4')
| -rw-r--r-- | ltac/extraargs.ml4 | 19 |
1 files changed, 2 insertions, 17 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index 4d3507cbc4..fbae17bafc 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -104,16 +104,14 @@ let glob_occs ist l = l let subst_occs evm l = l ARGUMENT EXTEND occurrences + TYPED AS int list PRINTED BY pr_int_list_full INTERPRETED BY interp_occs GLOBALIZED BY glob_occs SUBSTITUTED BY subst_occs - RAW_TYPED AS occurrences_or_var RAW_PRINTED BY pr_occurrences - - GLOB_TYPED AS occurrences_or_var GLOB_PRINTED BY pr_occurrences | [ ne_integer_list(l) ] -> [ ArgArg l ] @@ -141,10 +139,7 @@ ARGUMENT EXTEND glob GLOBALIZED BY glob_glob SUBSTITUTED BY subst_glob - RAW_TYPED AS constr_expr RAW_PRINTED BY pr_gen - - GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen [ constr(c) ] -> [ c ] END @@ -158,16 +153,14 @@ ARGUMENT EXTEND lconstr END ARGUMENT EXTEND lglob + TYPED AS glob PRINTED BY pr_globc INTERPRETED BY interp_glob GLOBALIZED BY glob_glob SUBSTITUTED BY subst_glob - RAW_TYPED AS constr_expr RAW_PRINTED BY pr_gen - - GLOB_TYPED AS glob_constr_and_expr GLOB_PRINTED BY pr_gen [ lconstr(c) ] -> [ c ] END @@ -207,9 +200,7 @@ ARGUMENT EXTEND hloc INTERPRETED BY interp_place GLOBALIZED BY intern_place SUBSTITUTED BY subst_place - RAW_TYPED AS loc_place RAW_PRINTED BY pr_loc_place - GLOB_TYPED AS loc_place GLOB_PRINTED BY pr_loc_place [ ] -> [ ConclLocation () ] @@ -224,12 +215,6 @@ ARGUMENT EXTEND hloc END - - - - - - (* Julien: Mise en commun des differentes version de replace with in by *) let pr_by_arg_tac _prc _prlc prtac opt_c = |