diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-15 07:56:21 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-15 07:56:21 +0000 |
| commit | b2c9129662f55eea46a8937f9fd0cfabc029457a (patch) | |
| tree | fb3cb41fe45c41b58149559228088607621c8007 /contrib | |
| parent | e4639721323887555d278b963b84b11244871632 (diff) | |
methode export
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -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 *) |