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/vernacentries.ml | |
| parent | d47ddf56bc93ae16280ce8a845a4b004fef52fb8 (diff) | |
| parent | a9728d5a43e5c82fed9cac25e841107c4c95fc35 (diff) | |
Merge PR #7898: Remove camlp4 remains
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 27f2a740e..b6bc76a2e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2040,7 +2040,7 @@ let vernac_load interp fname = interp x in let parse_sentence = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.Gram.entry_parse Pvernac.main_entry po with + match Pcoq.Entry.parse Pvernac.main_entry po with | Some x -> x | None -> raise End_of_input) in let fname = @@ -2049,7 +2049,7 @@ let vernac_load interp fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in - Pcoq.Gram.parsable ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in + Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in begin try while true do interp (snd (parse_sentence input)) done with End_of_input -> () |