The Coq mailing list

[Dimitri Hendriks <Dimitri.Hendriks AT phil.uu.nl>]

Hi,

In the file changes.html it is said that the condition for guarded fixpoints
has been extended and that it is now possible to define structural fixpoints
for positive inductive definitions with nested recursion.

But when I try the given example (after Require PolyList.):

        Inductive term : Set := fun : (list term)->term.

I get:

        Warning: Ignoring recursive call


What's wrong?


Dimitri