coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top"

From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top"
Date: Wed, 10 Feb 2016 11:23:55 +0100

Hello. I also raised this problem in

https://coq.inria.fr/bugs/show_bug.cgi?id=4541 .

Le 09/02/2016 19:55, Peter Vanderbilt a écrit :

In Coq8.5, coq_makefile adds "-R . Top” to COQLIBS and COQDOCLIBS. Why?
Doing so breaks coqtop in Emacs (Aquamacs), because the Require statements
fail — it expects module “X” but gets “Top.X”.

How do I get coq_makefile to not add "-R . Top” (as in 8.4)?
OR
How do I get the coqtop in emacs to have the right flags?

Pete

[Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/09/2016
- Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Frédéric Blanqui, 02/10/2016
  - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Clément Pit--Claudel, 02/10/2016
    - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/10/2016
      - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Clément Pit--Claudel, 02/10/2016
        
        Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/12/2016
        
        Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Clément Pit--Claudel, 02/12/2016
        
        [Coq-Club] GitHub's ProofGeneral has old version number, Peter Vanderbilt, 02/13/2016
        
        Re: [Coq-Club] GitHub's ProofGeneral has old version number, Clément Pit--Claudel, 02/13/2016
      - Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Tej Chajed, 02/10/2016
        
        Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Peter Vanderbilt, 02/12/2016
- Re: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top", Christian Doczkal, 02/10/2016