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

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

1 files changed, 14 insertions, 1 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index f2efb7cfa1..3aaba27579 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -363,8 +363,21 @@ end
 
 module Grammar = Register(GrammarObj)
 
+let warn_deprecated_intropattern =
+  let open CWarnings in
+  create ~name:"deprecated-intropattern-entry" ~category:"deprecated"
+  (fun () -> Pp.strbrk "Entry name intropattern has been renamed in order \
+  to be consistent with the documented grammar of tactics. Use \
+  \"simple_intropattern\" instead.")
+
+let check_compatibility = function
+  | Genarg.ExtraArg s when ArgT.repr s = "intropattern" -> warn_deprecated_intropattern ()
+  | _ -> ()
+
 let register_grammar = Grammar.register0
-let genarg_grammar = Grammar.obj
+let genarg_grammar x =
+  check_compatibility x;
+  Grammar.obj x
 
 let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
   let e = new_entry u s in