open Printf;;
+let debug_print = fun _ -> ()
+
type coercions = (UriManager.uri * UriManager.uri * UriManager.uri) list
(* the list of known coercions (MUST be transitively closed) *)
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
;;
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
!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 *)