diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-25 23:07:21 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-25 23:07:21 +0000 |
| commit | ae9b8392410ceb09e30c90c8863fc24a4c67b376 (patch) | |
| tree | feebabfa679409a5fbb06a6e01bdfd41a325297d /tactics | |
| parent | 10621555f900d25df4fd2f71b045a050f8eb9f90 (diff) | |
ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED
Rationale: the expansion ignores the TYPED clause when
{RAW,GLOB}_TYPED are given. Indeed, in this case, the final type is a
consequence of either "INTERPRETED BY" (if given), or the default one
based on GLOB_TYPED.
This avoids the pitfall of the "raw" argument extension, where the
TYPED clause was unused and totally misleading.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13760 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extraargs.ml4 | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 6bdbdb80b..76376cd03 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -40,7 +40,6 @@ let pr_int_list_full _prc _prlc _prt l = in aux l ARGUMENT EXTEND int_nelist - TYPED AS int list PRINTED BY pr_int_list_full RAW_TYPED AS int list RAW_PRINTED BY pr_int_list_full @@ -82,7 +81,6 @@ type occurrences_or_var = int list or_var type occurrences = int list ARGUMENT EXTEND occurrences - TYPED AS occurrences PRINTED BY pr_int_list_full INTERPRETED BY interp_occs @@ -113,7 +111,6 @@ let glob_raw = Tacinterp.intern_constr let subst_raw = Tacinterp.subst_glob_constr_and_expr ARGUMENT EXTEND raw - TYPED AS glob_constr PRINTED BY pr_rawc INTERPRETED BY interp_raw @@ -157,7 +154,6 @@ let interp_place ist gl = function let subst_place subst pl = pl ARGUMENT EXTEND hloc - TYPED AS place PRINTED BY pr_place INTERPRETED BY interp_place GLOBALIZED BY intern_place @@ -227,7 +223,6 @@ let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id) ARGUMENT EXTEND comma_var_lne - TYPED AS var list PRINTED BY pr_var_list_typed RAW_TYPED AS var list RAW_PRINTED BY pr_var_list @@ -238,7 +233,6 @@ ARGUMENT EXTEND comma_var_lne END ARGUMENT EXTEND comma_var_l - TYPED AS var list PRINTED BY pr_var_list_typed RAW_TYPED AS var list RAW_PRINTED BY pr_var_list @@ -260,7 +254,6 @@ END ARGUMENT EXTEND in_arg_hyp - TYPED AS var list option * bool PRINTED BY pr_in_arg_hyp_typed RAW_TYPED AS var list option * bool RAW_PRINTED BY pr_in_arg_hyp |