aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/g_indfun.mlg2
-rw-r--r--plugins/ltac/coretactics.mlg2
-rw-r--r--plugins/ltac/extraargs.mlg4
-rw-r--r--plugins/ltac/extratactics.mlg8
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/pltac.ml4
-rw-r--r--plugins/ltac/pptactic.ml13
-rw-r--r--plugins/ltac/tacarg.ml10
-rw-r--r--plugins/ltac/tacarg.mli7
-rw-r--r--plugins/ltac/taccoerce.ml79
-rw-r--r--plugins/ltac/tacintern.ml3
-rw-r--r--plugins/ltac/tacinterp.ml3
-rw-r--r--plugins/ltac/tacsubst.ml3
13 files changed, 85 insertions, 55 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 89a6655d03..ef9d91c7fa 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -83,7 +83,7 @@ let out_disjunctive = CAst.map (function
}
-ARGUMENT EXTEND with_names TYPED AS intropattern option PRINTED BY { pr_intro_as_pat }
+ARGUMENT EXTEND with_names TYPED AS intro_pattern option PRINTED BY { pr_intro_as_pat }
| [ "as" simple_intropattern(ipat) ] -> { Some ipat }
| [] -> { None }
END
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index 01817dc8f9..2159c05f80 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -150,7 +150,7 @@ TACTIC EXTEND specialize
| [ "specialize" constr_with_bindings(c) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
}
-| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> {
+| [ "specialize" constr_with_bindings(c) "as" simple_intropattern(ipat) ] -> {
Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
}
END
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 5a7ce4c3da..2654729652 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -35,7 +35,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr
-let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simple_intropattern
let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
let () =
let inject (loc, v) = Tacexpr.Tacexp v in
@@ -46,7 +46,7 @@ let () =
let () =
let register name entry = Tacentries.register_tactic_notation_entry name entry in
register "hyp" wit_var;
- register "simple_intropattern" wit_intro_pattern;
+ register "simple_intropattern" wit_simple_intropattern;
register "integer" wit_integer;
register "reference" wit_ref;
()
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index d385ccab5e..49d8ab4e23 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -174,15 +174,15 @@ TACTIC EXTEND einjection
| [ "einjection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) true c }
END
TACTIC EXTEND injection_as
-| [ "injection" "as" intropattern_list(ipat)] ->
+| [ "injection" "as" simple_intropattern_list(ipat)] ->
{ injClause None (Some (decode_inj_ipat ipat)) false None }
-| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
+| [ "injection" destruction_arg(c) "as" simple_intropattern_list(ipat)] ->
{ mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c }
END
TACTIC EXTEND einjection_as
-| [ "einjection" "as" intropattern_list(ipat)] ->
+| [ "einjection" "as" simple_intropattern_list(ipat)] ->
{ injClause None (Some (decode_inj_ipat ipat)) true None }
-| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
+| [ "einjection" destruction_arg(c) "as" simple_intropattern_list(ipat)] ->
{ mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c }
END
TACTIC EXTEND simple_injection
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 6033249435..5c84b35f1b 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -38,7 +38,7 @@ let arg_of_expr = function
let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat
+let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_simple_intropattern) pat
let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 28ab801ee2..e3042dc3cb 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -52,7 +52,9 @@ let () =
let open Stdarg in
let open Tacarg in
register_grammar wit_int_or_var (int_or_var);
- register_grammar wit_intro_pattern (simple_intropattern);
+ register_grammar wit_intro_pattern (simple_intropattern); (* To remove at end of deprecation phase *)
+(* register_grammar wit_intropattern (intropattern); *) (* To be added at end of deprecation phase *)
+ register_grammar wit_simple_intropattern (simple_intropattern);
register_grammar wit_quant_hyp (quantified_hypothesis);
register_grammar wit_uconstr (uconstr);
register_grammar wit_open_constr (open_constr);
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 4b6b192f0a..db8d09b79e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1314,6 +1314,12 @@ let pr_glob_constr_pptac env sigma c =
let pr_lglob_constr_pptac env sigma c =
pr_lglob_constr_env env c
+let pr_raw_intro_pattern =
+ lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)
+
+let pr_glob_intro_pattern =
+ lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c))
+
let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
@@ -1323,11 +1329,8 @@ let () =
pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
register_basic_print0 wit_var pr_lident pr_lident pr_id;
- register_print0
- wit_intro_pattern
- (lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma))
- (lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c)))
- pr_intro_pattern_env;
+ register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
+ register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env;
Genprint.register_print0
wit_clause_dft_concl
(lift (pr_clauses (Some true) pr_lident))
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index c9dbbea1ea..9e8e86d4fc 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -19,13 +19,19 @@ let make0 ?dyn name =
let () = Geninterp.register_val0 wit dyn in
wit
-let wit_intro_pattern = make0 "intropattern"
+let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *)
+let wit_simple_intropattern = make0 "simple_intropattern"
let wit_quant_hyp = make0 "quant_hyp"
let wit_constr_with_bindings = make0 "constr_with_bindings"
let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
let wit_bindings = make0 "bindings"
let wit_quantified_hypothesis = wit_quant_hyp
-let wit_intropattern = wit_intro_pattern
+
+(* A convenient common part to simple_intropattern and intropattern
+ usable when no parsing rule is concerned: indeed
+ simple_intropattern and intropattern are in the same type and have
+ the same interp/intern/subst methods *)
+let wit_intro_pattern = wit_intropattern
let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
make0 "tactic"
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index a631585e61..945f237c91 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -16,6 +16,12 @@ open Tactypes
open Tacexpr
(** Tactic related witnesses, could also live in tactics/ if other users *)
+(* To keep after deprecation phase but it will get a different parsing semantics in pltac.ml *)
+val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
+[@@ocaml.deprecated "Use wit_simple_intropattern"]
+
+val wit_simple_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
+
val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
@@ -36,7 +42,6 @@ val wit_bindings :
constr bindings delayed_open) genarg_type
val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
(** Generic arguments based on Ltac. *)
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 33b3da757a..4e79bab28e 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -144,9 +144,22 @@ let coerce_to_constr_context v =
out_gen (topwit wit_constr_context) v
else raise (CannotCoerceTo "a term context")
+let is_intro_pattern v =
+ if has_type v (topwit wit_intropattern [@warning "-3"]) then
+ Some (out_gen (topwit wit_intropattern [@warning "-3"]) v).CAst.v
+ else
+ if has_type v (topwit wit_simple_intropattern) then
+ Some (out_gen (topwit wit_simple_intropattern) v).CAst.v
+ else
+ None
+
(* Interprets an identifier which must be fresh *)
let coerce_var_to_ident fresh env sigma v =
let fail () = raise (CannotCoerceTo "a fresh identifier") in
+ match is_intro_pattern v with
+ | Some (IntroNaming (IntroIdentifier id)) -> id
+ | Some _ -> fail ()
+ | None ->
if has_type v (topwit wit_intro_pattern) then
match out_gen (topwit wit_intro_pattern) v with
| { CAst.v=IntroNaming (IntroIdentifier id)} -> id
@@ -170,11 +183,11 @@ let id_of_name = function
| Name.Anonymous -> Id.of_string "x"
| Name.Name x -> x in
let fail () = raise (CannotCoerceTo "an identifier") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | {CAst.v=IntroNaming (IntroIdentifier id)} -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
+ match is_intro_pattern v with
+ | Some (IntroNaming (IntroIdentifier id)) -> id
+ | Some _ -> fail ()
+ | None ->
+ if has_type v (topwit wit_var) then
out_gen (topwit wit_var) v
else
match Value.to_constr v with
@@ -209,9 +222,10 @@ let id_of_name = function
let coerce_to_intro_pattern sigma v =
- if has_type v (topwit wit_intro_pattern) then
- (out_gen (topwit wit_intro_pattern) v).CAst.v
- else if has_type v (topwit wit_var) then
+ match is_intro_pattern v with
+ | Some pat -> pat
+ | None ->
+ if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
IntroNaming (IntroIdentifier id)
else match Value.to_constr v with
@@ -227,11 +241,9 @@ let coerce_to_intro_pattern_naming sigma v =
| _ -> raise (CannotCoerceTo "a naming introduction pattern")
let coerce_to_hint_base v =
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | {CAst.v=IntroNaming (IntroIdentifier id)} -> Id.to_string id
- | _ -> raise (CannotCoerceTo "a hint base name")
- else raise (CannotCoerceTo "a hint base name")
+ match is_intro_pattern v with
+ | Some (IntroNaming (IntroIdentifier id)) -> Id.to_string id
+ | Some _ | None -> raise (CannotCoerceTo "a hint base name")
let coerce_to_int v =
if has_type v (topwit wit_int) then
@@ -240,12 +252,12 @@ let coerce_to_int v =
let coerce_to_constr env v =
let fail () = raise (CannotCoerceTo "a term") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | {CAst.v=IntroNaming (IntroIdentifier id)} ->
+ match is_intro_pattern v with
+ | Some (IntroNaming (IntroIdentifier id)) ->
(try ([], constr_of_id env id) with Not_found -> fail ())
- | _ -> fail ()
- else if has_type v (topwit wit_constr) then
+ | Some _ -> fail ()
+ | None ->
+ if has_type v (topwit wit_constr) then
let c = out_gen (topwit wit_constr) v in
([], c)
else if has_type v (topwit wit_constr_under_binders) then
@@ -269,11 +281,11 @@ let coerce_to_closed_constr env v =
let coerce_to_evaluable_ref env sigma v =
let fail () = raise (CannotCoerceTo "an evaluable reference") in
let ev =
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> EvalVarRef id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
+ match is_intro_pattern v with
+ | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id
+ | Some _ -> fail ()
+ | None ->
+ if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
else fail ()
@@ -308,11 +320,11 @@ let coerce_to_intro_pattern_list ?loc sigma v =
let coerce_to_hyp env sigma v =
let fail () = raise (CannotCoerceTo "a variable") in
- if has_type v (topwit wit_intro_pattern) then
- match out_gen (topwit wit_intro_pattern) v with
- | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> id
- | _ -> fail ()
- else if has_type v (topwit wit_var) then
+ match is_intro_pattern v with
+ | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id
+ | Some _ -> fail ()
+ | None ->
+ if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
if is_variable env id then id else fail ()
else match Value.to_constr v with
@@ -340,12 +352,11 @@ let coerce_to_reference sigma v =
(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
let coerce_to_quantified_hypothesis sigma v =
- if has_type v (topwit wit_intro_pattern) then
- let v = out_gen (topwit wit_intro_pattern) v in
- match v with
- | {CAst.v=IntroNaming (IntroIdentifier id)} -> NamedHyp id
- | _ -> raise (CannotCoerceTo "a quantified hypothesis")
- else if has_type v (topwit wit_var) then
+ match is_intro_pattern v with
+ | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id
+ | Some _ -> raise (CannotCoerceTo "a quantified hypothesis")
+ | None ->
+ if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
NamedHyp id
else if has_type v (topwit wit_int) then
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 0fa4dc8baf..3ed5b1aab2 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -795,7 +795,8 @@ let () =
let ist = { ist with ltacvars = !lf } in
(ist, ans)
in
- Genintern.register_intern0 wit_intro_pattern intern_intro_pattern
+ Genintern.register_intern0 wit_intropattern intern_intro_pattern [@warning "-3"];
+ Genintern.register_intern0 wit_simple_intropattern intern_intro_pattern
let () =
let intern_clause ist cl =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 12a31ad164..8ddf17ca14 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2029,7 +2029,8 @@ let () =
register_interp0 wit_pre_ident (lift interp_pre_ident);
register_interp0 wit_ident (lift interp_ident);
register_interp0 wit_var (lift interp_hyp);
- register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
+ register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"];
+ register_interp0 wit_simple_intropattern (lifts interp_intro_pattern);
register_interp0 wit_clause_dft_concl (lift interp_clause);
register_interp0 wit_constr (lifts interp_constr);
register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 69d29afd01..b6e7dd64b0 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -287,7 +287,8 @@ let () =
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
Genintern.register_subst0 wit_ident (fun _ v -> v);
Genintern.register_subst0 wit_var (fun _ v -> v);
- Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
+ Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"];
+ Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern;
Genintern.register_subst0 wit_tactic subst_tactic;
Genintern.register_subst0 wit_ltac subst_tactic;
Genintern.register_subst0 wit_constr subst_glob_constr;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:58:36 +0000