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.ml | |
| 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.ml')
| -rw-r--r-- | library/libobject.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index 1096ac43a..31fb81c57 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,16 +6,16 @@ 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 } type obj = Dyn.t (* persistent dynamic objects *) type dynamic_object_declaration = { dyn_cache_function : section_path * obj -> unit; - dyn_load_function : obj -> unit; - dyn_open_function : obj -> unit; + dyn_load_function : section_path * obj -> unit; + dyn_open_function : section_path * obj -> unit; dyn_specification_function : obj -> obj } let object_tag lobj = Dyn.tag lobj @@ -28,11 +28,11 @@ let declare_object (na,odecl) = let cacher (spopt,lobj) = if Dyn.tag lobj = na then odecl.cache_function(spopt,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the cachefun" - and loader lobj = - if Dyn.tag lobj = na then odecl.load_function (outfun lobj) + and loader (spopt,lobj) = + if Dyn.tag lobj = na then odecl.load_function (spopt,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the loadfun" - and opener lobj = - if Dyn.tag lobj = na then odecl.open_function (outfun lobj) + and opener (spopt,lobj) = + if Dyn.tag lobj = na then odecl.open_function (spopt,outfun lobj) else anomaly "somehow we got the wrong dynamic object in the openfun" and spec_extractor lobj = infun(odecl.specification_function (outfun lobj)) @@ -53,11 +53,11 @@ let apply_dyn_fun f lobj = let cache_object ((_,lobj) as node) = apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj -let load_object lobj = - apply_dyn_fun (fun d -> d.dyn_load_function lobj) lobj +let load_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_load_function node) lobj -let open_object lobj = - apply_dyn_fun (fun d -> d.dyn_open_function lobj) lobj +let open_object ((_,lobj) as node) = + apply_dyn_fun (fun d -> d.dyn_open_function node) lobj let extract_object_specification lobj = apply_dyn_fun (fun d -> d.dyn_specification_function lobj) lobj |