Avertissement contre les Require dans le corps d'une section

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1829 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 0 deletions

diff --git a/library/lib.ml b/library/lib.ml
index c46a3833bf..9438713d6c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -139,6 +139,10 @@ let start_module s =
 
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
+let sections_are_opened () =
+  try let _ = find_entry_p is_opened_section in true
+  with Not_found -> false
+
 let export_segment seg =
   let rec clean acc = function
     | (_,Module _) :: _ | [] -> acc