module Library

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 8 deletions

diff --git a/library/libobject.mli b/library/libobject.mli
index 967e4c410..7ddac57b2 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -5,20 +5,23 @@
 open Names
 (*i*)
 
-(* [Libobject] declares persistent objects given with three methods:
+(* [Libobject] declares persistent objects, given with three methods:
+   - a caching function specifying how to add the object in the current
+     scope of theory modules;
    - a loading function, specifying what to do when the object is loaded
      from the disk;
-   - a caching function specifying how to import the object in the current
-     scope of theory modules;
+   - an opening function, specifying what to do when the module containing
+     the object is opened;
    - a specification function, to extract its specification when writing
      the specification of a module to the disk (.vi) *)
 
 type 'a object_declaration = {
-  load_function : 'a -> unit;
   cache_function : section_path * 'a -> unit;
+  load_function : 'a -> unit;
+  open_function : 'a -> unit;
   specification_function : 'a -> 'a }
 
-(*s given the object-name, the "loading" function, the "caching" function, 
+(*s Given the object-name, the "loading" function, the "caching" function, 
    and the "specification" function, the function [declare_object]
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
@@ -30,8 +33,7 @@ val declare_object :
 
 val object_tag : obj -> string
 
-val load_object : obj -> unit
-
 val cache_object : (section_path * obj) -> unit
-
+val load_object : obj -> unit
+val open_object : obj -> unit
 val extract_object_specification : obj -> obj