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: Clément Pit--Claudel <clement.pit AT gmail.com>
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 08:32:03 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:mZPMPx3hBufFftPfsmDT+DRfVm0co7zxezQtwd8ZsegSL/ad9pjvdHbS+e9qxAeQG96LtLQf0aGK4ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZ/tnLzjs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGCCLZ34RVHkhqhtURk3u6BjnUpr1+n/xsud41S+Ge9X3UZg7XD2j6+FgTxq+23RPDCIw7GyC0p84t6lcuh/0/xE=

Which version of Proof General are you using? Does using the latest version
at https://github.com/ProofGeneral/PG fix the problem? If not, can you raise
an issue there with a small example?

Clément.

On 02/10/2016 05:23 AM, Frédéric Blanqui wrote:
> 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
>>
>
>

Attachment: signature.asc
Description: OpenPGP digital signature

[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