diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pcoq.ml | 15 |
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 |