(* 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