* http://helm.cs.unibo.it/
*)
+type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
+exception EqCarrNotImplemented of string Lazy.t
+exception EqCarrOnNonMetaClosed
+
let db = ref []
let use_coercions = ref true
+let coerc_carr_of_term t =
+ try
+ Uri (CicUtil.uri_of_term t)
+ with Invalid_argument _ ->
+ match t with
+ | Cic.Sort s -> Sort s
+ | t -> Term t
+;;
+
+let eq_carr src tgt =
+ match src, tgt with
+ | 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 ->
+ raise
+ (EqCarrNotImplemented
+ (lazy ("Unsupported carr for coercions: " ^
+ CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)))
+ | _ -> raise EqCarrOnNonMetaClosed
+
+let name_of_carr = function
+ | Uri u -> UriManager.name_of_uri u
+ | Sort s -> CicPp.ppsort s
+ | Term _ -> assert false
+
+
let to_list () =
!db