From 55d9e712c68a3b9eb7b83881095c8995542f8904 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 8 Oct 2009 10:11:18 +0000
Subject: 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
---
 library/lib.ml                | 14 +++++++-------
 test-suite/failure/Sections.v |  4 ++++
 2 files changed, 11 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/failure/Sections.v

diff --git a/library/lib.ml b/library/lib.ml
index 20c6bf1e49..961a4ebb99 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 0000000000..9b3b35c13b
--- /dev/null
+++ b/test-suite/failure/Sections.v
@@ -0,0 +1,4 @@
+Module A.
+Section	B.
+End A.
+End A.
-- 
cgit v1.2.3