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