diff options
| -rw-r--r-- | library/lib.ml | 14 | ||||
| -rw-r--r-- | test-suite/failure/Sections.v | 4 |
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. |