coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq-inferior or inferior-coq?

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] coq-inferior or inferior-coq?
Date: Fri, 15 Jul 2016 11:50:21 +0200
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:nK0RORMSW/zcZajFAYIl6mtUPXoX/o7sNwtQ0KIMzox0KP/yrarrMEGX3/hxlliBBdydsKMczbaK+Pm/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9aU05j8jr/60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9YwuxhX7vkm7otLVbjwV6U+V71RSjo8YE4v48i+nh1CSAaJ+kwkU3lT1zFMChXJ4RWyCpz1vy73sPY7wCiGFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==

On 2016-02-04 08:33, Alan Schmitt wrote:
> Hello,
>
> I’m looking at the babel org-mode integration for coq, and it uses
> inferior-coq. As I tried to load it, I noticed that the feature
> 'inferior-coq is provided by a file called coq-inferior.el. This is
> a bit inconvenient (as one cannot simply do a ~(require
> 'inferior-coq)~). Is there a reason for this naming difference?
>
> This is on 8.4, but I also see this in 8.5:
> https://github.com/coq/coq/blob/trunk/tools/coq-inferior.el#L324

Can you open a bug report for this? It looks like a bug with an easy fix (we
just need an extra `provide' in there) :)

Attachment: signature.asc
Description: OpenPGP digital signature

Re: [Coq-Club] coq-inferior or inferior-coq?, Clément Pit--Claudel, 07/15/2016