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/lib.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'library/lib.mli')

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