diff options
| -rw-r--r-- | toplevel/vernac.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d92f02ddd6..89bc31d0ac 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -229,9 +229,7 @@ let rec vernac_com verbose checknav (loc,com) = if do_beautify () then pr_new_syntax loc (Some com); if !Flags.time then display_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in - let a = Lexer.com_state () in - interp com; - Lexer.restore_com_state a + interp com with reraise -> let (reraise, info) = Errors.push reraise in Format.set_formatter_out_channel stdout; |