X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=00cfa90daea8859fadec8266f1f7946508060b9e;hb=46f19eadce5f3a11c0ae26934fd8d1b597906416;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..00cfa90da 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,13 +25,15 @@
 
 open Printf;;
 
-ignore(Helm_registry.load_from "/home/tassi/helm/gTopLevel/gTopLevel.conf.xml")
+let debug_print = fun _ -> ()
+
+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)",
@@ -58,13 +60,13 @@ let look_for_coercion src tgt =
         UriManager.eq t tgt) 
       !coercions 
     in
-    prerr_endline (sprintf ":) TROVATA la coercion %s %s" 
+    debug_print (sprintf ":) TROVATA la coercion %s %s" 
       (UriManager.name_of_uri src) 
       (UriManager.name_of_uri tgt));
     Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
   with 
     Not_found -> 
-      prerr_endline (sprintf ":( NON TROVATA la coercion %s %s" 
+      debug_print (sprintf ":( NON TROVATA la coercion %s %s" 
         (UriManager.name_of_uri src) (UriManager.name_of_uri tgt));
       None
 ;;
@@ -122,7 +124,7 @@ let generate_composite_closure c1 c2 univ =
     try 
       CicTypeChecker.type_of_aux' [] [] c univ
     with CicTypeChecker.TypeCheckerFailure s as exn ->
-      prerr_endline (sprintf "Generated composite coercion:\n%s\n%s" 
+      debug_print (sprintf "Generated composite coercion:\n%s\n%s" 
         (CicPp.ppterm c) s);
       raise exn
   in
@@ -188,29 +190,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 *)
-
-let l = close_coercion_graph 
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)")
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CAbGroups/CAbGroup.ind#xpointer(1/1)")
- (UriManager.uri_of_string
- "cic:/CoRN/algebra/CRings/cr_crr.con")
-in
- List.iter (fun (u,o,g) -> 
-   prerr_endline (CicPp.ppobj o);
-   prerr_endline (UriManager.string_of_uri u);
-   prerr_endline "")
- l
- 
- 
-
 (* EOF *)