-exception EqCarrNotImplemented of string Lazy.t
-exception EqCarrOnNonMetaClosed
-val eq_carr: coerc_carr -> coerc_carr -> bool
-val coerc_carr_of_term: Cic.term -> coerc_carr
-val name_of_carr: coerc_carr -> string
-val uri_of_carr: coerc_carr -> UriManager.uri option
+val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
+val string_of_carr: coerc_carr -> string
+
+(* takes a term in whnf ~delta:false and a desired ariety *)
+val coerc_carr_of_term: Cic.term -> int -> coerc_carr
+
+type coerc_db
+val empty_coerc_db : coerc_db
+val dump: unit -> coerc_db
+val restore: coerc_db -> unit