diff options
Diffstat (limited to 'contrib/interface/parse.ml')
| -rw-r--r-- | contrib/interface/parse.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 7648e79227..bdda47e38f 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -223,10 +223,9 @@ 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; ();; |