Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem with ProofGeneral

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with ProofGeneral


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page