| Uri src, Uri tgt -> UriManager.eq src tgt
| Sort (Cic.Type _), Sort (Cic.Type _) -> true
| Sort src, Sort tgt when src = tgt -> true
- | Term t1, Term t2 when
- CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 ->
+ | Term t1, Term t2 ->
+ if CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 then
raise
(EqCarrNotImplemented
(lazy ("Unsupported carr for coercions: " ^
CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
- | _ -> raise EqCarrOnNonMetaClosed
+ else raise EqCarrOnNonMetaClosed
+ | _, _ -> false
let name_of_carr = function
| Uri u -> UriManager.name_of_uri u
| Sort s -> CicPp.ppsort s
- | Term _ -> assert false
+ | Term t -> CicPp.ppterm t
let to_list () =