aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2016-04-27 22:13:04 +0200
committerHugo Herbelin2016-04-27 22:13:04 +0200
commitee46e2744d68dd7402d38cfbc63d1d523fce9cdc (patch)
treeaa3c05f348b7520ccfe407db1301788a55f58673
parent141296307ad81fd1f6d69c0827fd284a81587abc (diff)
Revert "Protect the beautifier from change in the lexer state (typically by"
This reverts commit f2192b492ca5407e740cf9d9d8696da89c978b93.
-rw-r--r--toplevel/vernac.ml4
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;