(* takes a term in whnf ~delta:false and a desired ariety *)
val coerc_carr_of_term: Cic.term -> int -> coerc_carr
-val to_list:
- unit ->
- (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
-
type coerc_db
+val empty_coerc_db : coerc_db
val dump: unit -> coerc_db
val restore: coerc_db -> unit
+val to_list:
+ coerc_db ->
+ (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list
+
(* src carr, tgt carr, uri, saturations, coerced position
* invariant:
* if the constant pointed by uri has n argments
(coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list
val is_a_coercion: Cic.term -> coercion_entry option
+
+val prefer: UriManager.uri -> unit