Cic.metasenv -> Cic.substitution -> Cic.context ->
Cic.term -> Cic.term -> coercion_search_result
-val look_for_coercion' :
- Cic.metasenv -> Cic.substitution -> Cic.context ->
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result
-
(* checks if term is a constant or
* a constant applyed that is marked with (`Class `Coercion) *)
val is_composite: Cic.term -> bool
(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
val meets :
Cic.metasenv -> Cic.substitution -> Cic.context ->
- CoercDb.coerc_carr -> CoercDb.coerc_carr ->
+ bool * CoercDb.coerc_carr -> bool * CoercDb.coerc_carr ->
(CoercDb.coerc_carr * Cic.metasenv *
(Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list