From d9e83b3701f9c90542810feb212aea3a6aa0f141 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 20 Nov 2001 18:37:13 +0000
Subject: hack temporaire concernant les remarks/modules

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2217 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extract_env.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 87e390116c..2fd9979868 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -26,7 +26,13 @@ open Common
   We just keep constants and inductives. *)
 
 let extract_module m =
-  let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in
+  let m = 
+    try 
+      Nametab.locate_loaded_library (Nametab.make_short_qualid m) 
+    with Not_found ->  
+      errorlabstrm "module_message"
+	[< 'sTR "Module"; 'sPC;pr_id m; 'sPC; 'sTR "not found." >] 
+    in
   let seg = Library.module_segment (Some m) in
   let get_reference = function
     | sp, Leaf o ->
@@ -72,7 +78,9 @@ let rec visit_reference m eenv r =
       let m_name = module_of_r r' in 
       if not (Idset.mem m_name eenv.modules) then begin
 	eenv.modules <- Idset.add m_name eenv.modules;
- 	List.iter (visit_reference m eenv) (extract_module m_name)
+ 	try (* HACK temporaire pour eviter les m_name qui sont des sections *)
+	  List.iter (visit_reference m eenv) (extract_module m_name)
+	with _ -> ()
       end
     end;
     visit_decl m eenv (extract_declaration r);
-- 
cgit v1.2.3