diff options
Diffstat (limited to 'contrib/interface/parse.ml')
| -rw-r--r-- | contrib/interface/parse.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index f1f04a2df5..7648e79227 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -190,7 +190,7 @@ let parse_string_action reqid phylum char_stream string_list = P_c (xlate_vernac (execute_when_necessary - (Gram.Entry.parse Pcoq.Vernac.vernac_eoi (Gram.parsable char_stream)))) + (Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream)))) | "TACTIC_COM" -> P_t (xlate_tactic (Gram.Entry.parse Pcoq.Tactic.tactic_eoi @@ -223,9 +223,10 @@ let parse_string_action reqid phylum char_stream string_list = let quiet_parse_string_action char_stream = - try let _ = - Gram.Entry.parse Pcoq.Vernac.vernac_eoi (Gram.parsable char_stream) in - () + try + let _ = + Gram.Entry.parse Pcoq.Vernac_.vernac_eoi (Gram.parsable char_stream) in + () with | _ -> flush_until_end_of_stream char_stream; ();; |