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

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

1 files changed, 3 insertions, 1 deletions

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);