aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--library/lib.ml1
-rw-r--r--toplevel/coqtop.ml2
2 files changed, 3 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml
index c5bc798d9..53c6e2b05 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -350,6 +350,7 @@ let end_compilation dir =
" and not " ^ (string_of_dirpath m));
in
let (after,_,before) = split_lib oname in
+ comp_name := None;
!path_prefix,after
(* Returns true if we are inside an opened module type *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f81a16616..1b75287b5 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -105,8 +105,10 @@ let add_compile verbose s =
Options.make_silent true;
compile_list := (verbose,s) :: !compile_list
let compile_files () =
+ let init_state = States.freeze() in
List.iter
(fun (v,f) ->
+ States.unfreeze init_state;
if Options.do_translate () then
with_option translate_file (Vernac.compile v) f
else