coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq IDE with jump to definition

From: Erik Martin-Dorel <e.mdorel AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq IDE with jump to definition
Date: Thu, 12 Jan 2017 20:23:51 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e.mdorel AT gmail.com; spf=Pass smtp.mailfrom=e.mdorel AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f45.google.com
Ironport-phdr: 9a23:PUmQ1h34bwaIuRNismDT+DRfVm0co7zxezQtwd8ZseIUK/ad9pjvdHbS+e9qxAeQG96Kt7Qf06GP6fyocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbQhFgDWwbal8IRmqogndq9cajIR/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksFwlqBUoByhqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4TzqEEOrRq9BQKxA+3g0CVIhmP33a08yugvHwbG3BY+ENIKrX/Zq8v6OL0XUe+oy6nI1yvMb/dN1Dfy7YjHaBEhofWWUb1sdsrRzFAiGgXYhVuerozlOima1uULs2WD4OpgVP6vi246qw5quDSg2sAsiozRioIQ0F/E7zl5wIczJdGhVUF7ZsSkH4VUty2AMIt2WMwiTmd1syg50r0LoYC3cDQOxZg9xBPSa+aLf5aV7h/sTuqcLjd1iXR4c7ylnRmy61KvyujkW8m0zllKqi1Fn8HJtn8X1hzT7tGLSvph/ku9wDqP2Q/e5+FeLUA7kqrbLJEhwroumZYJrUvDGSr2lF33jK+QaEok5vCl5/r7brjivJORNI95hhvgPqgzlcGzG+s1PwgWU2ie4+u81bnj/UPjQLVNi/07irfWvIrfJcsGoa65GRFa0oI45hawCjepytUYnX0dIF1ZfxKHipDlO0vSL/DgEfe/n1OsnS93yPDBJ73tG4nCLnzekLj6Zrt98E5dyA8rzd9F/Z5UC7cBIOjyWkDrrtDYAAU5YESIxLPsD8w43YcDU0qOBLWYOeXcqwyy6/orMtWLMYIPuTW7LvE/+//oyHM+g1IZVaSvxt4TeXe+WPN8LBa3e33p1/obEGRCmwMkUO3szXGFSzNXLyK/Gacw4Ss2DKqpCI7CQsamh7nXj3TzJYFfem0TUgPEKnzvbYjRA/o=

Dear Abhishek,

2017-01-12 18:03 GMT+01:00 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

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

You may also try the company-coq extension of ProofGeneral: jump to definition is bound to "Meta-."
cf. https://github.com/cpitclaudel/company-coq#outlines-code-folding-and-jumping-to-definition

Best regards,

Érik Martin-Dorel

http://erik.martin-dorel.org/

[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