The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Sorry for the flood 

> Let's omit the fact that there may be PARAMETERS as you do

return clause is not generalized against parameters you just have to change 

if expr has type T p_1 .. _p_k u_1 u_2 .. u_n then matchExpr has type 
RExpr/{x_1=u_1,x_2=u_2 .. x_n=u_n;y=expr}

if Ci has type forall z_1 .. z_k yi_1 .. yi_mi, T z_1 .. z_k v_1 .. v_n then 
Di has type RExpr/{x_1=v_1,x_2=v_2 .. x_n=v_n;y=Ci yi_1 .. yi_mi}

to deal with them.

Pierre B.