val generate_dot_file: unit -> string
+(* given the Appl contents returns the argument of the head coercion *)
+val coerced_arg: Cic.term list -> Cic.term option
+
+(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
val meets :
+ Cic.metasenv -> Cic.substitution -> Cic.context ->
CoercDb.coerc_carr -> CoercDb.coerc_carr ->
- CoercDb.coerc_carr list
+ (CoercDb.coerc_carr * Cic.metasenv *
+ (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list