coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq IDE with jump to definition

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Coq IDE with jump to definition
Date: Thu, 12 Jan 2017 12:03:28 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f174.google.com
Ironport-phdr: 9a23:zOqF7hCKtRldiy6VZdKeUyQJP3N1i/DPJgcQr6AfoPdwSP3ypMbcNUDSrc9gkEXOFd2CrakV16yN6+uxByRAuc/H6y9SNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUt2as8Pi3OervpbXfg8A0DG6ePZ5KAi8hQTXrMgfx4V4fPUf0BzM91JCe+VNxW5rbXuVlhDwrpO59p5i6CRduLQo8cdGXeP7frg3ZbNdBTUidWsy4Zu45lH4UQKT6y5EAS0tmR1SDl2d4Q==

Is there a Coq IDE that does "jump to definition", like the way merlin based OCaml IDEs do?

IIRC, for a file that is unedited since the last compilation, the .glob file produced by coqc already records much of the needed information, at least for the references to global constants.

(Also, thanks Bruno for your thorough response to all my questions in the other thread. It fixed some of my misunderstandings.)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] Coq IDE with jump to definition, Abhishek Anand, 01/12/2017
- Re: [Coq-Club] Coq IDE with jump to definition, Enrico Tassi, 01/12/2017
- Re: [Coq-Club] Coq IDE with jump to definition, Erik Martin-Dorel, 01/12/2017
  - Re: [Coq-Club] Coq IDE with jump to definition, Abhishek Anand, 01/16/2017