diff options
| author | Jasper Hugunin | 2019-05-07 15:04:04 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2019-05-10 12:23:32 -0700 |
| commit | beb5bdec79ff371f48a478df3c24f2cf9d68aa1f (patch) | |
| tree | 727cd1ef35cca121d784274ef8bf739ffac5cfc2 /vernac/metasyntax.mli | |
| parent | 8ee7a4a7003fc2c5b01e0d6041961b3da14c0c84 (diff) | |
Use Print Custom Grammar to inspect custom entries
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 |