diff options
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 |