From 3386a50c15ddc367cd247f288ff84f288a0c42af Mon Sep 17 00:00:00 2001 From: filliatr Date: Sat, 18 Sep 1999 16:13:36 +0000 Subject: module Library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@74 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libobject.mli | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'library/libobject.mli') 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 -- cgit v1.2.3