coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coqdoc and pretty-printing of imported notations

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Andrej Bauer <andrej.bauer AT andrej.com>, Coq Club <coq-club AT inria.fr>
Cc: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
Subject: Re: [Coq-Club] Coqdoc and pretty-printing of imported notations
Date: Tue, 8 Mar 2011 11:38:59 +0100

> Otherwise said, "coqdoc A.v B.v" will work.

Excellent. So then for example if I have a rather large library and
just one example usage of it, I cannot easily compile only the usage
file?

With kind regards,

Andrej

[Coq-Club] Coqdoc and pretty-printing of imported notations, Andrej Bauer
- Re: [Coq-Club] Coqdoc and pretty-printing of imported notations, Hugo Herbelin
  - Re: [Coq-Club] Coqdoc and pretty-printing of imported notations, Andrej Bauer