coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: "Yevgeniy Makarov" <emakarov AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Two simple questions about coqdoc
Date: Wed, 24 Oct 2007 20:35:20 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=Q0AG4Dx1Pu8PoFs8hpBheqiy4FmTlK9nq2IAQ07g68LquSu4aamhCiwKrM1a/1ZqXtCqi9nV/QbOjVExQ189AU3tectDFUNbhoQWsZvp9SUfLDExE/E7P3Q95WaNEZETdIT11sFxmd50N7PK5vtVU9ock47hrh9x3G2wmQFrlcs=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

To remove the proofs from a Coq file, you can run the "gallina"
program on it. See section 13.8 in the reference manual.

Evgeny

[Coq-Club] Two simple questions about coqdoc, Edsko de Vries
- Re: [Coq-Club] Two simple questions about coqdoc, Brian Aydemir
  - Re: [Coq-Club] Two simple questions about coqdoc, Edsko de Vries
    - Re: [Coq-Club] Two simple questions about coqdoc, Yevgeniy Makarov
    - Re: [Coq-Club] Two simple questions about coqdoc, Edsko de Vries