The Coq mailing list

[Coq Dev <coqletsgo AT yahoo.com>]

Thank you very much, it works. When reading the error message, I thought it 
was just stating something impossible to be done (or that required extra 
assumptions, such as proof irrelevance).

(and sorry about the name confusion, it should be better now)

--- En date de : Mer 21.12.11, Pierre Courtieu 
<Pierre.Courtieu AT cnam.fr>
 a écrit :

> De: Pierre Courtieu 
>Â <Pierre.Courtieu AT cnam.fr>
> Objet: Re: [Coq-Club] Decidable equality on PositiveSets
> À: "Coq Dev" 
>Â <coqletsgo AT yahoo.com>
> Cc: 
>Â coq-club AT inria.fr
> Date: Mercredi 21 décembre 2011, 10h34
> 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.
> 
>