From e6307a2803c014e14ba8223512fb8416d8bc6269 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Jul 2001 18:59:47 +0000
Subject: Backtrack sur le warning Require en Section: trop contraignant

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

diff --git a/library/library.ml b/library/library.ml
index bea05a2229..a6b7b50127 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -200,8 +200,10 @@ let (in_require, _) =
        export_function = (fun _ -> None) })
   
 let require_module spec name fileopt export =
+(* Trop contraignant
   if sections_are_opened () then
     warning ("Objets of "^name^" not surviving sections (e.g. Grammar \nand Hints) will be removed at the end of the section");
+*)
   let file = match fileopt with
     | None -> name
     | Some f -> f 
-- 
cgit v1.2.3