| SomeCoercion of Cic.term
| NoCoercion
| NotMetaClosed
- | NotHandled of string
+ | NotHandled of string Lazy.t
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
* (source, list of coercions to follow, target)
*)
let get_closure_coercions src tgt uri coercions =
+ let eq_carr s t =
+ try
+ CoercDb.eq_carr s t
+ with
+ | CoercDb.EqCarrNotImplemented _ | CoercDb.EqCarrOnNonMetaClosed -> false
+ in
match src,tgt with
| CoercDb.Uri _, CoercDb.Uri _ ->
let c_from_tgt =
- List.filter (fun (f,_,_) -> CoercDb.eq_carr f tgt) coercions
+ List.filter (fun (f,_,_) -> eq_carr f tgt) coercions
in
let c_to_src =
- List.filter (fun (_,t,_) -> CoercDb.eq_carr t src) coercions
+ List.filter (fun (_,t,_) -> eq_carr t src) coercions
in
(List.map (fun (_,t,u) -> src,[uri; u],t) c_from_tgt) @
(List.map (fun (s,_,u) -> s,[u; uri],tgt) c_to_src) @
CicTypeChecker.type_of_aux' [] [] c univ
with CicTypeChecker.TypeCheckerFailure s as exn ->
debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s"
- (CicPp.ppterm c) s));
+ (CicPp.ppterm c) (Lazy.force s)));
raise exn
in
let cleaned_ty =