diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7ca51db78..41c496a6b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1969,7 +1969,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 Pcoq.main_entry po with + match Pcoq.Gram.entry_parse Pvernac.main_entry po with | Some x -> x | None -> raise End_of_input) in let fname = |