open Printf;;
+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)",
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 *)