coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Two simple questions about coqdoc

From: Edsko de Vries <devriese AT cs.tcd.ie>
To: Brian Aydemir <baydemir AT cis.upenn.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Two simple questions about coqdoc
Date: Wed, 24 Oct 2007 15:15:40 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Oct 24, 2007 at 10:11:23AM -0400, Brian Aydemir wrote:
> On Oct 24, 2007, at 10:01 AM, Edsko de Vries wrote:
>
> >- Is it possible to get coqdoc to skip all the proofs, but leave
> >  definitions in? So, if I have something like
> >
> >  Definition e := ..
> >
> >  or especially something like
> >
> >  Fixpoint f ..
> >
> >  is should should their definitions, but in
> >
> >  Theorem foo :=
> >  Proof.
> >  ...
> >  Qed.
> >
> >  Everything from 'Proof' to 'Qed' should be skipped.
>
> Try giving the --gallina (or -g for short) flag to coqdoc.  That
> should do what you want here.

Thanks for the quick reply. However, when I specify -g, definitions and
fixpoints disappear along with the proofs.

Edsko

[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