Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".

This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual

After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.

Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.

13 files changed, 85 insertions, 55 deletions

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index c217ed8b1d..9be2a5fe62 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 d9338f0421..e566d36e3c 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 eb9cacb975..a5b116c372 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 7ba63f1830..89dbda75bb 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 afdea98ef5..f435f82480 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 759bb62fdd..c309b5d907 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 79f0f521cc..bf0ce1e964 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 8a25d4851f..10f0e7f3cc 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 0c7096a4de..e091167a7b 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 fcab98c7e8..91a4bb20a8 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 7434f81946..8480be912d 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 4a0b01bcdc..d5cb0cad50 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 a3eeca2267..d0b75f558f 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;