The Coq mailing list

[Gábor Bakos <aborgabor AT gmail.com>]

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 yesterday.
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 see no signs of 8.2 at the home
page of Coq.)

Regarding the FAQ: The question 68 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.

?
Some of the questions (ex.: 133, 135, 144)
remain unanswered. Are those intentional? (As I remember yesterday
these were also unanswered, so it seems to be not a later corrected
behaviour.) I am not sure are these should go to the bug tracking
system?

I miss an entry regarding the cardinality related formulation. I
would like to reason about finite sets' cardinality. Is it well
supported? (Actually I am afraid some of the first FAQ answers should
answered my question, but I am not as well trained in this field to get
the proper conclusion easily.)
The tool seems to be great! Thanks, gabor

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, ...)