checked in new version of matita from svn

[helm.git] / helm / ocaml / cic_unification / coercGraph.ml

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index e256a19b82545562e990493c72429c7c85b3effc..6aad3676d11176fa045cc26ebfed4df9190b92cb 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,13 +25,13 @@
 
 open Printf;;
 
-ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
+type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
 
 (* the list of known coercions (MUST be transitively closed) *)
 let coercions = ref [
   (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)",
    UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con",
-   UriManager.uri_of_string "cic://Coq/Reals/Raxioms/INR.con") ;
+   UriManager.uri_of_string "cic:/Coq/Reals/Raxioms/INR.con") ;
 
    (
      UriManager.uri_of_string "cic:/CoRN/algebra/CFields/CField.ind#xpointer(1/1)",
@@ -188,11 +188,12 @@ let close_coercion_graph src tgt uri =
                 ((src,tgt,c_uri),(c_uri,named_obj,u))
       ) todo_list)
   in
-  coercions := !coercions @ new_coercions;
+  coercions := !coercions @ new_coercions @ [src,tgt,uri];
   new_coercions_obj
 ;;
 
-
+let get_coercions_list () =
+  !coercions
 
 
 (* stupid case *)