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.

4 files changed, 2 insertions, 27 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 =
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index ba9f82fb96..0b475340e2 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -980,9 +980,7 @@ let interp_test ist gls = function
 ARGUMENT EXTEND test
   PRINTED BY pr_itest'
   INTERPRETED BY interp_test
-  RAW_TYPED AS test
   RAW_PRINTED BY pr_test'
-  GLOB_TYPED AS test
   GLOB_PRINTED BY pr_test'
 | [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ]
 END
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index bc98b7d6d4..d4fd8a1df3 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -174,7 +174,6 @@ END
 let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
 
 ARGUMENT EXTEND hints_path_atom
-  TYPED AS hints_path_atom
   PRINTED BY pr_hints_path_atom
 | [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
 | [ "*" ] -> [ Hints.PathAny ]
@@ -183,7 +182,6 @@ END
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 
 ARGUMENT EXTEND hints_path
-  TYPED AS hints_path
   PRINTED BY pr_hints_path
 | [ "(" hints_path(p) ")"  ] -> [ p ]
 | [ "!" hints_path(p)  ] -> [ Hints.PathStar p ]
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index c4ef1f297e..395c2cd1b6 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -47,10 +47,7 @@ ARGUMENT EXTEND glob_constr_with_bindings
     GLOBALIZED BY glob_glob_constr_with_bindings
     SUBSTITUTED BY subst_glob_constr_with_bindings
 
-    RAW_TYPED AS constr_expr_with_bindings
     RAW_PRINTED BY pr_constr_expr_with_bindings
-
-    GLOB_TYPED AS glob_constr_with_bindings
     GLOB_PRINTED BY pr_glob_constr_with_bindings
 
    [ constr_with_bindings(bl) ] -> [ bl ]
@@ -76,10 +73,7 @@ ARGUMENT EXTEND rewstrategy
     GLOBALIZED BY glob_strategy
     SUBSTITUTED BY subst_strategy
 
-    RAW_TYPED AS raw_strategy
     RAW_PRINTED BY pr_raw_strategy
-
-    GLOB_TYPED AS glob_strategy
     GLOB_PRINTED BY pr_glob_strategy
 
     [ glob(c) ] -> [ StratConstr (c, true) ]