diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-22 14:02:22 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-22 14:02:22 +0000 |
commit | 2debc4ab0b171963afff40cc3183e4e92cca9a0e (patch) | |
tree | 5731b43d962a6cb731ca2b3295a863be083bd7be /library/libobject.ml | |
parent | b8c9be5ae052c936d069630a7480fd3691c1aad0 (diff) |
Correct implementation of discharging of implicit arguments and add new
setting "Set Manual Implicit Arguments" for manual-only implicits.
Fix test-suite script. This removes the discharge_info argument of
"dynamic" object's rebuild function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libobject.ml')
-rw-r--r-- | library/libobject.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index b24a46e38..684607b4b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -28,8 +28,6 @@ let relax b = relax_flag := b;; type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a -type discharge_info = (identifier * bool * bool) list - type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; @@ -38,7 +36,7 @@ type 'a object_declaration = { classify_function : object_name * 'a -> 'a substitutivity; subst_function : object_name * substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; - rebuild_function : discharge_info * 'a -> 'a; + rebuild_function : 'a -> 'a; export_function : 'a -> 'a option } let yell s = anomaly s @@ -52,7 +50,7 @@ let default_object s = { yell ("The object "^s^" does not know how to substitute!")); classify_function = (fun (_,obj) -> Keep obj); discharge_function = (fun _ -> None); - rebuild_function = (fun (_,x) -> x); + rebuild_function = (fun x -> x); export_function = (fun _ -> None)} @@ -78,7 +76,7 @@ type dynamic_object_declaration = { dyn_subst_function : object_name * substitution * obj -> obj; dyn_classify_function : object_name * obj -> obj substitutivity; dyn_discharge_function : object_name * obj -> obj option; - dyn_rebuild_function : discharge_info * obj -> obj; + dyn_rebuild_function : obj -> obj; dyn_export_function : obj -> obj option } let object_tag lobj = Dyn.tag lobj @@ -116,8 +114,8 @@ let declare_object odecl = Option.map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" - and rebuild (varinfo,lobj) = - if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj)) + and rebuild lobj = + if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the rebuildfun" and exporter lobj = if Dyn.tag lobj = na then @@ -174,7 +172,7 @@ let classify_object ((_,lobj) as node) = let discharge_object ((_,lobj) as node) = apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj -let rebuild_object ((_,lobj) as node) = +let rebuild_object (lobj as node) = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj let export_object lobj = |