From 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 Mon Sep 17 00:00:00 2001 From: filliatr Date: Sun, 19 Sep 1999 14:17:35 +0000 Subject: - un effort sur la doc (ocamlweb) - module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type 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@76 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libobject.mli | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'library/libobject.mli') diff --git a/library/libobject.mli b/library/libobject.mli index 7ddac57b2..ff076ee39 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,14 +6,14 @@ open Names (*i*) (* [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; - - 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) *) + 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; + 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 = { cache_function : section_path * 'a -> unit; @@ -21,8 +21,7 @@ type 'a object_declaration = { open_function : 'a -> unit; specification_function : 'a -> 'a } -(*s Given the object-name, the "loading" function, the "caching" function, - and the "specification" function, the function [declare_object] +(*s Given an object name and a declaration, the function [declare_object] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) -- cgit v1.2.3