The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

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

Thanks,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Athmospheric CO₂ (Updated February 1, 2016, Mauna Loa Obs.): 402.43 ppm

Attachment: signature.asc
Description: PGP signature