diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-26 12:27:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-26 12:27:42 +0000 |
| commit | 75effdc265e716651c860d0878ffbfc205646cbd (patch) | |
| tree | 9a3c1182c8678c6f57c42af92c6d617ff17957aa /contrib/ring | |
| parent | 03875d3a79dcb97616e402a148fa5930fb13f013 (diff) | |
Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@765 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/ring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index cac953b38..cada4f3fc 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -147,7 +147,7 @@ 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 = (fun _ -> ()); + { load_function = cache_th; open_function = (fun _ -> ()); cache_function = cache_th; specification_function = spec_th }) |