Fixed a bug introduced in revision 12265.

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

2 files changed, 11 insertions, 7 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 20c6bf1e4..961a4ebb9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -14,9 +14,6 @@ open Libnames
 open Nameops
 open Libobject
 open Summary
-
-
-
 type node =
   | Leaf of obj
   | CompilingLibrary of object_prefix
@@ -418,10 +415,13 @@ let is_module () =
 
 (* Returns the opening node of a given name *)
 let find_opening_node id =
-  try snd (find_entry_p (is_opened id))
-  with Not_found ->
-  try ignore (find_entry_p is_opening_node); error "There is nothing to end."
-  with Not_found -> error "Nothing to end of this name."
+  try
+    let oname,entry = find_entry_p is_opening_node in
+    let id' = basename (fst oname) in
+    if id <> id' then
+      error ("Last block to end has name "^(Names.string_of_id id')^".");
+    entry
+  with Not_found -> error "There is nothing to end."
 
 (* Discharge tables *)
 
diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v
new file mode 100644
index 000000000..9b3b35c13
--- /dev/null
+++ b/test-suite/failure/Sections.v
@@ -0,0 +1,4 @@
+Module A.
+Section	B.
+End A.
+End A.