aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEnrico Tassi2015-05-29 15:41:51 +0200
committerEnrico Tassi2015-05-29 15:44:47 +0200
commit43aa642ad4f2d30029c1c1f272ba162b6801a40b (patch)
treeaa3b4281a63483b5aaf99de5dbd1e0b3ef712ebd
parente47c30bf431f3c8160b41384eedb538ba16578d0 (diff)
coqtop: reset the current file name after a load-vernac-source
-rw-r--r--toplevel/vernac.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a06702e0d6..7d84ecf6ca 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -277,6 +277,7 @@ and read_vernac_file verbosely s =
close_input in_chan input; (* we must close the file first *)
match e with
| End_of_input ->
+ cur_file := None;
if do_beautify () then
pr_new_syntax (Loc.make_loc (max_int,max_int)) None
| _ -> raise_with_file fname (disable_drop e, info)