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)",
((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)")
prerr_endline (UriManager.string_of_uri u);
prerr_endline "")
l
-
+*)
(* EOF *)