diff options
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 240147c8d..33e6229b2 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -49,7 +49,7 @@ let entry_buf = Buffer.create 64 let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in - let () = Pcoq.Gram.entry_print ft e in + let () = Pcoq.Entry.print ft e in str (Buffer.contents entry_buf) let pr_registered_grammar name = |