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.

5 files changed, 4 insertions, 11 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index fdeef5f0ac..ff106404c8 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -138,9 +138,7 @@ let warn_deprecated_syntax =
 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
-  GLOB_TYPED AS reference_list
   GLOB_PRINTED BY pr_firstorder_using_glob
 | [ "using" reference(a) ] -> [ [a] ]
 | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index a2d31780dd..272852d47a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -48,9 +48,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings option
   PRINTED BY pr_fun_ind_using_typed
-  RAW_TYPED AS constr_with_bindings_opt
   RAW_PRINTED BY pr_fun_ind_using
-  GLOB_TYPED AS constr_with_bindings_opt
   GLOB_PRINTED BY pr_fun_ind_using
 | [ "using" constr_with_bindings(c) ] -> [ Some c ]
 | [ ] -> [ None ]
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 ]
 | [ ] -> [ [] ]
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 989a6c5bf1..d62656f95f 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -491,9 +491,10 @@ let mkhintref ?loc c n = match c.CAst.v with
   | _ -> mkAppC (c, mkCHoles ?loc n)
 
 ARGUMENT EXTEND ssrhintref
-                             PRINTED BY pr_ssrhintref
-    RAW_TYPED AS constr  RAW_PRINTED BY pr_raw_ssrhintref
-   GLOB_TYPED AS constr GLOB_PRINTED BY pr_glob_ssrhintref
+  TYPED AS constr
+  PRINTED BY pr_ssrhintref
+  RAW_PRINTED BY pr_raw_ssrhintref
+  GLOB_PRINTED BY pr_glob_ssrhintref
   | [ constr(c) ] -> [ c ]
   | [ constr(c) "|" natural(n) ] -> [ mkhintref ~loc c n ]
 END