From 3b75964509a52ec779f64ebded388cc35da1a806 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
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 +
 1 file changed, 1 insertion(+)

(limited to 'library')

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 *)
-- 
cgit v1.2.3