From ec66fade3f217897338cb0012eb06145d809edc8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 20 Dec 2000 19:50:39 +0000
Subject: Test pour empêcher 2 sections de même noms

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1172 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml      | 3 +++
 library/nametab.ml  | 3 +++
 library/nametab.mli | 1 +
 3 files changed, 7 insertions(+)

diff --git a/library/lib.ml b/library/lib.ml
index 4d95bdce9c..53b5a21b04 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Libobject
@@ -106,6 +107,8 @@ let contents_after = function
 
 let open_section s =
   let sp = make_path (id_of_string s) OBJ in
+  if Nametab.exists_module sp then
+    errorlabstrm "open_section" [< 'sTR (s^" already exists") >];
   add_entry sp (OpenedSection (s, freeze_summaries()));
   path_prefix := !path_prefix @ [s];
   sp
diff --git a/library/nametab.ml b/library/nametab.ml
index 7b92a40cca..57002455b7 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -164,6 +164,9 @@ let rec rec_open_module_contents qid =
 let exists_cci sp =
   try let _ = locate (qualid_of_sp sp) in true with Not_found -> false
 
+let exists_module sp =
+  try let _ = locate_module (qualid_of_sp sp) in true with Not_found -> false
+
 (********************************************************************)
 (* Registration of persistent tables as a global table and rollback *)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 13c6b514bd..7f43b9d843 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -35,6 +35,7 @@ val locate_module : qualid -> section_path * module_contents
 
 (* [exists sp] tells if [sp] is already bound to a cci term *)
 val exists_cci : section_path -> bool
+val exists_module : section_path -> bool
 
 val open_module_contents : qualid -> unit
 val rec_open_module_contents : qualid -> unit
-- 
cgit v1.2.3