coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] problem with ProofGeneral

From: Michel Levy <Michel.Levy AT imag.fr>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] problem with ProofGeneral
Date: Wed, 04 Sep 2002 18:42:58 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: LSR

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.

        Sincerely yours

--
Michel Levy
Laboratoire L.S.R., Bureau C214, B.P.72 - 38042 SAINT MARTIN D'HERES
CEDEX
e.mail :
Michel.Levy AT imag.fr
    tel :(33)476514022
http://www-lsr.imag.fr/users/Michel.Levy

[Coq-Club] problem with ProofGeneral, Michel Levy
- Re: [Coq-Club] problem with ProofGeneral, Pierre Courtieu