The Coq mailing list

[Julien Narboux <Julien AT narboux.fr>]

Hi,

Gábor Bakos a écrit :
> Hi All,
>
> (Newbie post, non-native English speaker sorry about it.)
> (Sorry if double post, the previous went to the mailto address from
> the contact page 
> (coq-club_NS AT pauillac.inria.fr)
>  which seems to be not
> correct. At least it resulted a mail delivery failure.)
> I was able to download 8.2 sources from the homepage of Coq at last
> weekend. Was it accidental? The build sais it is 8.2 (February 2009).
> If I remember well those sources were marked as stable. Was that
> release revoked or it was just a dream ;)? (I have seen no signs of
> 8.2 at the home page of Coq till yesterday.)
>   
You were not dreaming ;-)

> Regarding the FAQ: The question 69 has a little confusing answer.
> Would not it be better choice what does the error message means? Or
> finishing by
> cut (b*a <>0 -> a<>0).
> cut (b*a <>0 -> b<>0).
> auto.
> auto with real.
> auto with real.
> Qed.
> or
> firstorder.
> Qed.
> ?
>   

Thanks, you are right, the problem wad due to a change of the semantics 
of the field tactic.

> Some of the questions (ex.: 133, 135, 144) remain unanswered. Are
> those intentional?

No, thanks for reporting this.  In the svn/trunk version of the faq, i 
have added an answer to the question about 'dependency graph' and 
deleted the other unanswered questions.

> I miss an entry regarding the cardinality related formulation. I would
> like to reason about finite sets' cardinality. Is it well supported?
>   
You can get some results about cardinality of finite sets here :

http://logical.saclay.inria.fr/coq/distrib/current/stdlib/Coq.Sets.Finite_sets_facts.html

> PS.: Is not somewhere an eclipse plugin like Proof General for Coq?
> (It would be interesting to see some of the XText features, like
> context sensitive completion, content based hilighting, maybe model
> transformation to MathML, ...)
>
>   
Have a look here : http://provereditor.gforge.inria.fr/

Best wishes,

Julien