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

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