coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <Pierre.Courtieu AT sophia.inria.fr>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] problem with ProofGeneral
- Date: Wed, 4 Sep 2002 19:10:23 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
On Wed, 04 Sep 2002 18:42:58 +0200
Michel Levy
<Michel.Levy AT imag.fr>
wrote:
> In the README.coq of ProofGeneral, I have found :
>
> Generate a TAGS file for the library by running
> coqtags `find . -name \*.v -print`
> in the root directory of the library, $COQTOP/theories.
>
> But in that directory the theories are compiled (with the suffix .vo).
> What I have to do to generate the TAGS file.
You probably got a binary distribution of coq, so you cannot generate tags
until you download the sources. See http://coq.inria.fr/.
$COQTOP designates the root directory of coq sources (.v files).
Sincerly
Pierre
- [Coq-Club] problem with ProofGeneral, Michel Levy
- Re: [Coq-Club] problem with ProofGeneral, Pierre Courtieu
Archive powered by MhonArc 2.6.16.