diff options
| -rw-r--r-- | toplevel/coqtop.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
2 files changed, 6 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8f50bfb3d8..41d370ea57 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -641,6 +641,9 @@ let init_toplevel arglist = init_library_roots (); load_vernac_obj (); require (); + (* XXX: This is incorrect in batch mode, as we will initialize + the STM before having done Declaremods.start_library, thus + state 1 is invalid. This bug was present in 8.5/8.6. *) Stm.init (); let sid = load_rcfile (Stm.get_current_state ()) in (* XXX: We ignore this for now, but should be threaded to the toplevels *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index cf0e8e759f..deb2cc1e3f 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -164,7 +164,9 @@ let rec interp_vernac sid (loc,com) = let com = if !Flags.time then VernacTime (loc,com) else com in interp com with reraise -> - ignore(Stm.edit_at sid); + (* XXX: In non-interactive mode edit_at seems to do very weird + things, so we better avoid it while we investigate *) + if not !Flags.batch_mode then ignore(Stm.edit_at sid); let (reraise, info) = CErrors.push reraise in let loc' = Option.default Loc.ghost (Loc.get_loc info) in if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) |