The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Nothing wrong, it is just an information that the automatically
generated term_rec elimination does not take into account the 
recursive call. You have to write by hand your own elimination
principle using fixpoints. 

Christine.
In his message of Thu November 18, 1999, Dimitri Hendriks writes: 
> 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

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84