The Coq mailing list

[Cuihtlauac ALVARADO <alvarado AT labri.u-bordeaux.fr>]

Hello,

We, at Bordeaux, are a bit surprized by the following session :

Welcome to Coq V6.2 (January 1998)

Coq < Require PolyList.  
[Reinterning PolyList ...done]
[Reinterning Le ...done]

Coq < Inductive tree : Set :=
Coq < leaf : tree
Coq < | root : (list tree)->tree.
Warning: Ignoring recursive call
tree_ind is defined
tree_rec is defined
tree_rect is defined
tree is defined

First, I would have expected (following Coq's RM, p76) something like :

Error: Non positive Occurrence in (list tree)->tree

But P. Casteran pointed me that this definition of trees might be seen
as well-founded (and it must be, it's ok).

So, what ? :)
        
What is the difference between this definition and the classical one
(with mutual inductive types).

What is the exact meaning of the warning ?

What should I expect of an object of such a type ?

how/why/when should I prefer to choose such a definition instead of the
mutual inductive one ?

Best regards,

-- 
Cuihtlauac ALVARADO