diff options
Diffstat (limited to 'contrib/ring/ring.ml')
| -rw-r--r-- | contrib/ring/ring.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index f82cb6417..2a817668e 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -145,12 +145,12 @@ let _ = let (theory_to_obj, obj_to_theory) = let cache_th (_,(c, th)) = theories_map_add (c,th) - and spec_th x = x in + and export_th x = Some x in declare_object ("tactic-ring-theory", { load_function = (fun _ -> ()); open_function = cache_th; cache_function = cache_th; - specification_function = spec_th }) + export_function = export_th }) (* from the set A, guess the associated theory *) (* With this simple solution, the theory to use is automatically guessed *) |