Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations in favor of "simple_intropattern"

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

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;