diff options
| author | Maxime Dénès | 2018-07-19 11:41:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 18:41:11 +0100 |
| commit | 264c208a5eb824c880ef4c46e060185470064df5 (patch) | |
| tree | ce99aabb06f6232d4ecfd2117269d827df24463c /interp | |
| parent | dfd4c4a2b50edf894a19cd50c43517e1804eadc9 (diff) | |
Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/declare.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index a0ebc3775e..6778fa1e7a 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -445,11 +445,9 @@ let assumption_message id = (** Monomorphic universes need to survive sections. *) let input_universe_context : Univ.ContextSet.t -> Libobject.obj = - declare_object - { (default_object "Monomorphic section universes") with - cache_function = (fun (na, uctx) -> Global.push_context_set false uctx); - discharge_function = (fun (_, x) -> Some x); - classify_function = (fun a -> Dispose) } + declare_object @@ local_object "Monomorphic section universes" + ~cache:(fun (na, uctx) -> Global.push_context_set false uctx) + ~discharge:(fun (_, x) -> Some x) let declare_universe_context poly ctx = if poly then |