From f3d068d8bd33a511397576533b1190be9b544a07 Mon Sep 17 00:00:00 2001 From: filliatr Date: Sun, 19 Sep 1999 18:01:50 +0000 Subject: module Declare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@77 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libobject.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'library/libobject.ml') 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 -- cgit v1.2.3