diff options
Diffstat (limited to 'plugins/ring/ring.ml')
| -rw-r--r-- | plugins/ring/ring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 9a252dfb7..98d6361c0 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -262,7 +262,7 @@ let subst_th (subst,(c,th as obj)) = (c',th') -let theory_to_obj = +let theory_to_obj : constr * theory -> obj = let cache_th (_,(c, th)) = theories_map_add (c,th) in declare_object {(default_object "tactic-ring-theory") with open_function = (fun i o -> if i=1 then cache_th o); |