aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/ring/ring.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index cada4f3fc..f82cb6417 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -147,8 +147,8 @@ let (theory_to_obj, obj_to_theory) =
let cache_th (_,(c, th)) = theories_map_add (c,th)
and spec_th x = x in
declare_object ("tactic-ring-theory",
- { load_function = cache_th;
- open_function = (fun _ -> ());
+ { load_function = (fun _ -> ());
+ open_function = cache_th;
cache_function = cache_th;
specification_function = spec_th })