aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.md5
-rw-r--r--grammar/argextend.mlp43
-rw-r--r--plugins/firstorder/g_ground.ml42
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/g_auto.ml42
-rw-r--r--plugins/ssr/ssrvernac.ml47
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:39:11 +0000