diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 01:33:53 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 01:33:53 +0200 |
| commit | e372f0e5f0646eb4209baa06c874b4f041ed6574 (patch) | |
| tree | 0eb3b9bc736d4e5cdcd022b315cf7c2a4f0731a0 /vernac/metasyntax.ml | |
| parent | d47ddf56bc93ae16280ce8a845a4b004fef52fb8 (diff) | |
| parent | a9728d5a43e5c82fed9cac25e841107c4c95fc35 (diff) | |
Merge PR #7898: Remove camlp4 remains
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 = |