The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 28 Oct 2009, Stéphane Lescuyer wrote:

> I've thought about this as well and I agree this would be beneficial.
> There have been questions on this list of users who have defined a
> map-like function without generalizing the uniform parameters, and
> then could not figure out why they couldn't use it in a nested
> fixpoint.
>
> To ensure easier backwards compatibility, we could have an "Automatic
> Generalization on/off" vernacular to toggle the feature on or off.

It would be better to (eventually) have it on by default because we want 
to make avaiable fixpoints with higher order uniform parameters from 
people who haven't even though about others reusing their work.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''