Coercions are now generalized to the general form
f: \forall xs:Ts. \forall a:A xs. \forall ys:Ts'. B xs a ys
where f is declared as a coercion from A ? to B ? ? ? using the syntax
coercion uri arity saturations
where:
1. arity and saturations are optional with default 0
2. the saturations option is the number of ys
Useful example: it is now possible to declare a coercion from
nat to \exists n:nat. 0 \leq n
obtaining something extremely close to Russel (the new implementation of
the Program tactic of Coq) up to the fact that coercions are not propagated
yet under mutcases and fixes.
TODO: composition of coercions having saturations <> 0 is not implemented
yet (but should be easy to do, at least on paper)