diff options
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 |