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 /pretyping | |
| parent | dfd4c4a2b50edf894a19cd50c43517e1804eadc9 (diff) | |
Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f8e8fa9eb9..9c9877fd23 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -69,11 +69,9 @@ let subst_reduction_effect (subst,(con,funkey)) = (subst_constant subst con,funkey) let inReductionEffect : Constant.t * string -> obj = - declare_object {(default_object "REDUCTION-EFFECT") with - cache_function = cache_reduction_effect; - open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o); - subst_function = subst_reduction_effect; - classify_function = (fun o -> Substitute o) } + declare_object @@ global_object_nodischarge "REDUCTION-EFFECT" + ~cache:cache_reduction_effect + ~subst:(Some subst_reduction_effect) let declare_reduction_effect funkey f = if String.Map.mem funkey !effect_table then |