From 80b2afbc757f1d536e9663d702097be9477bee34 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 20 Nov 2000 08:43:47 +0000
Subject: Open est maintenant géré par Nametab
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@869 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/library.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library/library.mli')

diff --git a/library/library.mli b/library/library.mli
index cac8767d5..6d4bb1ed5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -30,7 +30,8 @@ val require_module : bool option -> string -> string option -> bool -> unit
 (*s [save_module_to s f] saves the current environment as a module [s]
   in the file [f]. *)
 
-val save_module_to : string -> string -> unit
+val save_module_to : (Lib.library_segment -> Nametab.module_contents) -> 
+  string -> string -> unit
 
 (*s [module_segment m] returns the segment of the loaded module
     [m]; if not given, the segment of the current module is returned
-- 
cgit v1.2.3