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.

7 files changed, 29 insertions, 34 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index f30b4107b6..c5632411d1 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -27,6 +27,11 @@ Coqlib:
   command then enables to locate the registered constant through its name. The
   name resolution is dynamic.
 
+Macros:
+
+- The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
+  deprecated. Use TYPED AS instead.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 9c25dcfaba..d6fe91e8a7 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -81,38 +81,35 @@ let make_extend loc s cl wit = match cl with
       let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in
       $lid:s$ >>
 
-let warning_redundant prefix s =
-  Printf.eprintf "Redundant [%sTYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" prefix s
+let warning_deprecated prefix s = function
+| None -> ()
+| Some _ ->
+  Printf.eprintf "Deprecated [%sTYPED AS] clause in [ARGUMENT EXTEND %s]. \
+                  Use [TYPED AS] instead.\n%!" prefix s
 
-let get_type prefix s = function
+let get_type s = function
 | None -> None
 | Some typ ->
   if is_self s typ then
-    let () = warning_redundant prefix s in None
+    let () = Printf.eprintf "Redundant [TYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" s in
+    None
   else Some typ
 
-let check_type prefix s = function
-| None -> ()
-| Some _ -> warning_redundant prefix s
-
 let declare_tactic_argument loc s (typ, f, g, h) cl =
   let se = mlexpr_of_string s in
-  let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with
+  let typ, rawpr, globpr, pr = match typ with
     | `Uniform (typ, pr) ->
-      let typ = get_type "" s typ in
-      typ, pr, typ, pr, typ, pr
+      let typ = get_type s typ in
+      typ, pr, pr, pr
     | `Specialized (a, rpr, c, gpr, e, tpr) ->
-      (** Check that we actually need the TYPED AS arguments *)
-      let rawtyp = get_type "RAW_" s a in
-      let glbtyp = get_type "GLOB_" s c in
-      let toptyp = get_type "" s e in
-      let () = match g with None -> () | Some _ -> check_type "RAW_" s rawtyp in
-      let () = match f, h with Some _, Some _ -> check_type "GLOB_" s glbtyp | _ -> () in
-      rawtyp, rpr, glbtyp, gpr, toptyp, tpr
+      let () = warning_deprecated "RAW_" s a in
+      let () = warning_deprecated "GLOB_" s c in
+      let toptyp = get_type s e in
+      toptyp, rpr, gpr, tpr
   in
   let glob = match g with
     | None ->
-      begin match rawtyp with
+      begin match typ with
       | None -> <:expr< fun ist v -> (ist, v) >>
       | Some rawtyp ->
         <:expr< fun ist v ->
@@ -126,9 +123,9 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
   in
   let interp = match f with
     | None ->
-      begin match globtyp with
+      begin match typ with
       | None ->
-        let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
+        let typ = match typ with None -> ExtraArgType s | Some typ -> typ in
         <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >>
       | Some globtyp ->
         <:expr< fun ist x ->
@@ -136,7 +133,7 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
       end
     | Some f ->
       (** Compatibility layer, TODO: remove me *)
-      let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in
+      let typ = match typ with None -> ExtraArgType s | Some typ -> typ in
       <:expr<
         let f = $lid:f$ in
         fun ist v -> Ftactic.enter (fun gl ->
@@ -147,7 +144,7 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
       >> in
   let subst = match h with
     | None ->
-      begin match globtyp with
+      begin match typ with
       | None -> <:expr< fun s v -> v >>
       | Some globtyp ->
         <:expr< fun s x ->
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