The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

On Sat, Nov 12, 2011 at 05:04:13PM +0100, Alexandre Pilkiewicz wrote:

> I just finished a big proof, typed the Qed., waited a few second for
> the type checking of the term to finish, and then... nothing! I wanted
> to celebrate, to share my happiness with the world, I wanted to dance.

Congrats for your Qed! I hope to get mine in a couple of months. I have
been working for a proof since eight months.

> But there is no Qed dance :(

Sure, something is missing. Each time I finish an important lemma, it is
like a new baby, but nobody cares.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/