From 6d8d2c2f3941a9be486f225d9b62239a6a9113a1 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 5 May 2010 12:27:48 +0000
Subject: Patch bug 2313. Including a module or module type into the top
 module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12994 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/library/lib.ml b/library/lib.ml
index dcf7e70cd6..34be607fec 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -262,13 +262,19 @@ let is_opening_node = function
     _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true
   | _ -> false
 
+let is_opening_node_or_lib = function
+    _,(CompilingLibrary _ | OpenedSection _ 
+    | OpenedModule _ | OpenedModtype _) -> true
+  | _ -> false
 
 let current_mod_id () =
-  try match find_entry_p is_opening_node with
+  try match find_entry_p is_opening_node_or_lib with
     | oname,OpenedModule (_,_,fs) ->
 	basename (fst oname)
     | oname,OpenedModtype (_,fs) ->
 	basename (fst oname)
+    | oname,CompilingLibrary _ ->
+       basename (fst oname)
     | _ -> error "you are not in a module"
   with Not_found ->
     error "no opened modules"
-- 
cgit v1.2.3