X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=712e8aae2d46b7e95ddf1520cc9b41e011b223e5;hb=b41886e9d21d756279bd6a2ec3f19c17b1a64401;hp=e01f28eb3fcc1994f068dbc86926e6dff42a614c;hpb=e8236af508187f6446f5af481d545d433628ee00;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index e01f28eb3..712e8aae2 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,8 +25,6 @@
 
 open Printf;;
 
-ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
-
 (* 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)",
@@ -188,15 +186,16 @@ 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 *)
-
+(*
 let l = close_coercion_graph 
  (UriManager.uri_of_string
  "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
@@ -210,7 +209,7 @@ in
    prerr_endline (UriManager.string_of_uri u);
    prerr_endline "")
  l
- 
+*) 
  
 
 (* EOF *)