From 3b75964509a52ec779f64ebded388cc35da1a806 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 13 Jul 2004 18:35:43 +0000
Subject: bug #780: compilation of several units in the same coqtop process

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5900 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml     | 1 +
 toplevel/coqtop.ml | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/library/lib.ml b/library/lib.ml
index c5bc798d9b..53c6e2b059 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 f81a16616e..1b75287b5b 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
-- 
cgit v1.2.3