From 7befcc7ea63ea4bd6e45e6f4b8ec01a69b586cc7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sun, 24 Aug 2014 11:17:00 +0200
Subject: Fix Declaremods.end_library (Closes: #3536)

---
 library/declaremods.ml | 3 ++-
 library/lib.ml         | 5 ++++-
 library/lib.mli        | 4 +++-
 3 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/library/declaremods.ml b/library/declaremods.ml
index e4f227637..bf6fe9f0d 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -874,8 +874,9 @@ let start_library dir =
   Lib.add_frozen_state ()
 
 let end_library dir =
+  let oname = Lib.end_compilation_checks dir in
   let mp,cenv,ast = Global.export dir in
-  let prefix, lib_stack = Lib.end_compilation dir in
+  let prefix, lib_stack = Lib.end_compilation oname in
   assert (ModPath.equal mp (MPfile dir));
   let substitute, keep, _ = Lib.classify_segment lib_stack in
   cenv,(substitute,keep),ast
diff --git a/library/lib.ml b/library/lib.ml
index 1ee3ca57b..f33f244b8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -313,7 +313,7 @@ let start_compilation s mp =
   comp_name := Some s;
   path_prefix := prefix
 
-let end_compilation dir =
+let end_compilation_checks dir =
   let _ =
     try match snd (find_entry_p is_opening_node) with
       | OpenedSection _ -> error "There are some open sections."
@@ -338,6 +338,9 @@ let end_compilation dir =
 	    (str "The current open module has name" ++ spc () ++ pr_dirpath m ++
              spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
   in
+  oname
+
+let end_compilation oname =
   let (after,mark,before) = split_lib_at_opening oname in
   comp_name := None;
   !path_prefix,after
diff --git a/library/lib.mli b/library/lib.mli
index 615a39f9e..b5a32f762 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -127,7 +127,9 @@ val end_modtype :
 (** {6 Compilation units } *)
 
 val start_compilation : Names.DirPath.t -> Names.module_path -> unit
-val end_compilation : Names.DirPath.t -> Libnames.object_prefix * library_segment
+val end_compilation_checks : Names.DirPath.t -> Libnames.object_name
+val end_compilation :
+  Libnames.object_name-> Libnames.object_prefix * library_segment
 
 (** The function [library_dp] returns the [DirPath.t] of the current
    compiling library (or [default_library]) *)
-- 
cgit v1.2.3