diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9d8bbcc00..48829288f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -910,7 +910,7 @@ let vernac_print = function | PrintFullContext -> msg (print_full_context_typ ()) | PrintSectionContext qid -> msg (print_sec_context_typ qid) | PrintInspect n -> msg (inspect n) - | PrintGrammar (uni,ent) -> Metasyntax.print_grammar uni ent + | PrintGrammar ent -> Metasyntax.print_grammar ent | PrintLoadPath -> (* For compatibility ? *) print_loadpath () | PrintModules -> msg (print_modules ()) | PrintModule qid -> print_module qid |