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

4 files changed, 26 insertions, 31 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 90116180eb..3266fcf9af 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -129,24 +129,22 @@ let make_prod_item = function
 let make_rule loc (prods,act) =
   <:expr< ($mlexpr_of_list make_prod_item prods$,$make_act loc act prods$) >>
 
-let declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr cl =
-  let rawtyp, rawpr = match rawtyppr with
-    | None -> typ,pr
-    | Some (t,p) -> t,p in
-  let globtyp, globpr = match globtyppr with
-    | None -> typ,pr
-    | Some (t,p) -> t,p in
+let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
+  let rawtyp, rawpr, globtyp, globpr = match typ with
+    | `Uniform typ -> typ, pr, typ, pr
+    | `Specialized (a, b, c, d) -> a, b, c, d
+  in
   let glob = match g with
     | None ->
 	<:expr< fun e x ->
-          out_gen $make_globwit loc typ$
+          out_gen $make_globwit loc rawtyp$
             (Tacinterp.intern_genarg e
                (Genarg.in_gen $make_rawwit loc rawtyp$ x)) >>
     | Some f -> <:expr< $lid:f$>> in
   let interp = match f with
     | None ->
 	<:expr< fun ist gl x ->
-          out_gen $make_wit loc typ$
+          out_gen $make_wit loc globtyp$
             (Tacinterp.interp_genarg ist gl
                (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
     | Some f -> <:expr< $lid:f$>> in
@@ -218,27 +216,33 @@ EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "ARGUMENT"; "EXTEND"; s = entry_name;
-        "TYPED"; "AS"; typ = argtype;
-        "PRINTED"; "BY"; pr = LIDENT;
-        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
-        g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
-        h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ];
-        rawtyppr =
-        (* Necessary if the globalized type is different from the final type *)
-          OPT [ "RAW_TYPED"; "AS"; t = argtype;
-                "RAW_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ];
-        globtyppr =
-          OPT [ "GLOB_TYPED"; "AS"; t = argtype;
-                "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ];
+        header = argextend_header;
         OPT "|"; l = LIST1 argrule SEP "|";
         "END" ->
-         declare_tactic_argument loc s typ pr f g h rawtyppr globtyppr l
+         declare_tactic_argument loc s header l
       | "VERNAC"; "ARGUMENT"; "EXTEND"; s = entry_name;
         pr = OPT ["PRINTED"; "BY"; pr = LIDENT -> pr];
         OPT "|"; l = LIST1 argrule SEP "|";
         "END" ->
          declare_vernac_argument loc s pr l ] ]
   ;
+  argextend_header:
+    [ [ "TYPED"; "AS"; typ = argtype;
+        "PRINTED"; "BY"; pr = LIDENT;
+        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
+        g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
+        h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ] ->
+        (`Uniform typ, pr, f, g, h)
+      | "PRINTED"; "BY"; pr = LIDENT;
+        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
+        g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
+        h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ];
+        "RAW_TYPED"; "AS"; rawtyp = argtype;
+        "RAW_PRINTED"; "BY"; rawpr = LIDENT;
+        "GLOB_TYPED"; "AS"; globtyp = argtype;
+        "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
+        (`Specialized (rawtyp, rawpr, globtyp, globpr), pr, f, g, h) ] ]
+  ;
   argtype:
     [ "2"
       [ e1 = argtype; "*"; e2 = argtype -> PairArgType (e1, e2) ]
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c77950c74d..c1b7b63c3e 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -109,7 +109,6 @@ let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_loc
 let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global
 
 ARGUMENT EXTEND firstorder_using
-  TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
   RAW_TYPED AS reference_list
   RAW_PRINTED BY pr_firstorder_using_raw
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index fb053c032f..39f4cf07f3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -56,7 +56,6 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
 
 
 ARGUMENT EXTEND fun_ind_using
-  TYPED AS constr_with_bindings_opt
   PRINTED BY pr_fun_ind_using_typed
   RAW_TYPED AS constr_with_bindings_opt
   RAW_PRINTED BY pr_fun_ind_using
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 6bdbdb80ba..76376cd033 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