diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-19 18:01:50 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-19 18:01:50 +0000 |
| commit | f3d068d8bd33a511397576533b1190be9b544a07 (patch) | |
| tree | d941947b2fdd5ba13a6f83a0814a3a74b666ea86 /library/libobject.mli | |
| parent | 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 (diff) | |
module Declare
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libobject.mli')
| -rw-r--r-- | library/libobject.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/libobject.mli b/library/libobject.mli index ff076ee39..d855059fa 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -17,8 +17,8 @@ open Names type 'a object_declaration = { cache_function : section_path * 'a -> unit; - load_function : 'a -> unit; - open_function : 'a -> unit; + load_function : section_path * 'a -> unit; + open_function : section_path * 'a -> unit; specification_function : 'a -> 'a } (*s Given an object name and a declaration, the function [declare_object] @@ -32,7 +32,7 @@ val declare_object : val object_tag : obj -> string -val cache_object : (section_path * obj) -> unit -val load_object : obj -> unit -val open_object : obj -> unit +val cache_object : section_path * obj -> unit +val load_object : section_path * obj -> unit +val open_object : section_path * obj -> unit val extract_object_specification : obj -> obj |