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 /library/keys.ml | |
| parent | 4ecbad30c77316294c8625ead722d469c1c7f79d (diff) | |
| parent | 264c208a5eb824c880ef4c46e060185470064df5 (diff) | |
Merge PR #8096: Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'library/keys.ml')
| -rw-r--r-- | library/keys.ml | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/library/keys.ml b/library/keys.ml index 53447a679a..58883ccc88 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -100,18 +100,13 @@ let discharge_keys (_,(k,k')) = | Some x, Some y -> Some (x, y) | _ -> None -let rebuild_keys (ref,ref') = (ref, ref') - type key_obj = key * key let inKeys : key_obj -> obj = - declare_object {(default_object "KEYS") with - cache_function = cache_keys; - load_function = load_keys; - subst_function = subst_keys; - classify_function = (fun x -> Substitute x); - discharge_function = discharge_keys; - rebuild_function = rebuild_keys } + declare_object @@ superglobal_object "KEYS" + ~cache:cache_keys + ~subst:(Some subst_keys) + ~discharge:discharge_keys let declare_equiv_keys ref ref' = Lib.add_anonymous_leaf (inKeys (ref,ref')) |