diff options
| author | Enrico Tassi | 2018-12-13 09:27:39 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-13 09:27:39 +0100 |
| commit | d9a6d4814f0669b586ca5c13d6d6540cd194b45f (patch) | |
| tree | f0f8582ff2c85eee0e7b42e253ad8358912c7f12 /plugins/funind | |
| parent | 4ecbad30c77316294c8625ead722d469c1c7f79d (diff) | |
| parent | 264c208a5eb824c880ef4c46e060185470064df5 (diff) | |
Merge PR #8096: Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 19f954c10d..5d0d17ee6b 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -237,7 +237,6 @@ let cache_Function (_,finfos) = from_graph := Indmap.add finfos.graph_ind finfos !from_graph -let load_Function _ = cache_Function let subst_Function (subst,finfos) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst_ind i = Mod_subst.subst_ind subst i @@ -271,9 +270,6 @@ let subst_Function (subst,finfos) = is_general = finfos.is_general } -let classify_Function infos = Libobject.Substitute infos - - let discharge_Function (_,finfos) = Some finfos let pr_ocst c = @@ -302,15 +298,11 @@ let pr_table tb = Pp.prlist_with_sep fnl pr_info l let in_Function : function_info -> Libobject.obj = - Libobject.declare_object - {(Libobject.default_object "FUNCTIONS_DB") with - Libobject.cache_function = cache_Function; - Libobject.load_function = load_Function; - Libobject.classify_function = classify_Function; - Libobject.subst_function = subst_Function; - Libobject.discharge_function = discharge_Function -(* Libobject.open_function = open_Function; *) - } + let open Libobject in + declare_object @@ superglobal_object "FUNCTIONS_DB" + ~cache:cache_Function + ~subst:(Some subst_Function) + ~discharge:discharge_Function let find_or_none id = |