diff options
Diffstat (limited to 'vernac/metasyntax.mli')
| -rw-r--r-- | vernac/metasyntax.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 38dbdf7e41..6435df23c7 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> (** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t +val pr_custom_grammar : string -> Pp.t val check_infix_modifiers : syntax_modifier list -> unit |