(* to apply the coercion it is sufficient to unify the last coercion
argument (that is a Meta) with the term to be coerced *)
| SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list
+ | SomeCoercionToTgt of (Cic.metasenv * Cic.term * Cic.term) list
| NoCoercion
- | NotMetaClosed
- | NotHandled of string Lazy.t
+ | NotHandled
val look_for_coercion :
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
-
val source_of: Cic.term -> Cic.term
-val generate_dot_file: unit -> string
+val generate_dot_file: Format.formatter -> unit
+(* given the Appl contents returns the argument of the head coercion *)
+val coerced_arg: Cic.term list -> (Cic.term * int) option
+
+(* returns: (carr,menv,(saturated coercion,last arg)option,idem) list *)
val meets :
- CoercDb.coerc_carr -> CoercDb.coerc_carr ->
- CoercDb.coerc_carr list
+ Cic.metasenv -> Cic.substitution -> Cic.context ->
+ bool * CoercDb.coerc_carr -> bool * CoercDb.coerc_carr ->
+ (CoercDb.coerc_carr * Cic.metasenv *
+ (Cic.term * Cic.term) option * (Cic.term * Cic.term) option) list