diff options
Diffstat (limited to 'library/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/library/libobject.mli b/library/libobject.mli index c0d89e4d..57c3debe 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,30 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libobject.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Libnames open Mod_subst -(*i*) -(* [Libobject] declares persistent objects, given with methods: +(** [Libobject] declares persistent objects, given with methods: * a caching function specifying how to add the object in the current scope; If the object wishes to register its visibility in the Nametab, - it should do so for all possible sufixes. + it should do so for all possible suffixes. * a loading function, specifying what to do when the module containing the object is loaded; If the object wishes to register its visibility in the Nametab, - it should do so for all sufixes no shorter than the "int" argument + it should do so for all suffixes no shorter than the "int" argument * an opening function, specifying what to do when the module containing the object is opened (imported); @@ -39,7 +35,7 @@ open Mod_subst the module name must be updated Keep - the object is not substitutive, but survives module closing - Anticipate - this is for objects that have to be explicitely + Anticipate - this is for objects that have to be explicitly managed by the [end_module] function (like Require and Read markers) @@ -74,7 +70,7 @@ type 'a object_declaration = { discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } -(* The default object is a "Keep" object with empty methods. +(** The default object is a "Keep" object with empty methods. Object creators are advised to use the construction [{(default_object "MY_OBJECT") with cache_function = ... @@ -85,18 +81,22 @@ type 'a object_declaration = { val default_object : string -> 'a object_declaration -(* the identity substitution function *) +(** the identity substitution function *) val ident_subst_function : substitution * 'a -> 'a -(*s Given an object declaration, the function [declare_object] +(** {6 ... } *) +(** Given an object declaration, the function [declare_object_full] will hand back two functions, the "injection" and "projection" functions for dynamically typed library-objects. *) type obj -val declare_object : +val declare_object_full : 'a object_declaration -> ('a -> obj) * (obj -> 'a) +val declare_object : + 'a object_declaration -> ('a -> obj) + val object_tag : obj -> string val cache_object : object_name * obj -> unit |