coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Peter Vanderbilt <acm AT petervanderbilt.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] why does coq_makefile in 8.5 add "-R . Top"
Date: Tue, 9 Feb 2016 10:55:27 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=acm AT petervanderbilt.com; spf=None smtp.mailfrom=acm AT petervanderbilt.com; spf=None smtp.helo=postmaster AT delivery.mailspamprotection.com
Ironport-phdr: 9a23:e51PNBODmIQ2nVF5+TYl6mtUPXoX/o7sNwtQ0KIMzox0KPj+rarrMEGX3/hxlliBBdydsKIbzbGO+Pm5ByQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokbvqsMSKPU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4kX3kbiFJ2Cg7J4QvwX5Pt+n/zve9VwCSGMNfoRLY4VC6o7qN3DhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

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