The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

This is due to the presence of "Local Unset Elimination Schemes" in
MSetPositive.v. which means that elimination schemes are not generated
automatically when tree is defined. Someone will probably tell us the
reason for this. In the same file later there is an explicit:

Scheme tree_ind := Induction for tree Sort Prop.

Which builds one for sort Prop. You can build the same for sort Set in
you own file:

Scheme tree_rec := Induction for PositiveSet.tree Sort Set.

Then your induction will work.

P.

PS Your name "Coq Dev" is confusing, as it is the name of a mailing
list. Please consider changing it.


2011/12/21 Coq Dev 
<coqletsgo AT yahoo.com>:
> Lemma l: forall (p p' : PositiveSet.t), {p = p'} + {p <> p'}.
> Proof.
>  induction p.