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/setoid_ring | |
| parent | 4ecbad30c77316294c8625ead722d469c1c7f79d (diff) | |
| parent | 264c208a5eb824c880ef4c46e060185470064df5 (diff) | |
Merge PR #8096: Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 9fea3ddcda..65201d922f 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -394,13 +394,9 @@ let subst_th (subst,th) = let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in - declare_object - {(default_object "tactic-new-ring-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x)} - + declare_object @@ global_object_nodischarge "tactic-new-ring-theory" + ~cache:cache_th + ~subst:(Some subst_th) let setoid_of_relation env evd a r = try @@ -891,12 +887,9 @@ let subst_th (subst,th) = let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in - declare_object - {(default_object "tactic-new-field-theory") with - open_function = (fun i o -> if Int.equal i 1 then cache_th o); - cache_function = cache_th; - subst_function = subst_th; - classify_function = (fun x -> Substitute x) } + declare_object @@ global_object_nodischarge "tactic-new-field-theory" + ~cache:cache_th + ~subst:(Some subst_th) let field_equality evd r inv req = match EConstr.kind !evd req with |