coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [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: Re: [Coq-Club] Coq IDE with jump to definition
Date: Mon, 16 Jan 2017 12:13:17 -0500
Authentication-results: mail3-smtp-sop.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-f177.google.com
Ironport-phdr: 9a23:5ohABRGqD1zv24jDQy1wTJ1GYnF86YWxBRYc798ds5kLTJ7zr8WwAkXT6L1XgUPTWs2DsrQf2raQ6P2rAzVQqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLd9IRmsowjctsYajZV/Jqsy1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrxCvpxJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6xaZYEAeobPeZfqonwv0cDogC+BQmtH+PvyiFHhnzr1qAm1eQuCwfG0xE9FN8Jqnvbt9X1NKYJUeC10qbIzi/PYOlQ2Tjn7ojHbwotofCNXbJsfsrc0kYvFwbfgVWRrYzpJS+a1uMIs2WC6edrSOyhi2kiqw5rozivwN8hhZXOhoIPzFDL6yF5wIIvKdKmVUF7fMaoEJRXtyGdOIt2Rt0tT3t0tyY9z70KoZG7fCkWyJQn2h7QcOaLfJSP4hLmTOqRJC13hGh5eLK+gRa+6FWvyurmVsaq1FZGtC1FksPDtn0Lyhfd6dCHR+Nj8ku93TuDzQPe5+FeLUwqiKbWKoQtzqMym5cRt0nIAzX4l1/sjKCMc0Up4uio5PrjYrXhvpKcMpV7igD6Mqg3g8y/Hfg0PhEAX2SG++mx1qfv/UL+QLVNgf02lrfWvIrGKsQco661Gw5V0oA95BajFzqqzsgUkH0dIF9GeB+LlZblN0zPLfziEPuygVahnC9ux//cP73hBpvNLmLEkLfkZbty8VVTyAoyzdBE55JbFLIBLOjpVU/3rtPYCAI2Pxa1w+bmFNV92ZgTWW2KAqCDMaPStUWE6f4oI+mJfIMVoiryK+A55/7yin80gUMSfa6w3ZcOdH+4GulmLF6CbHr3gtYBFH8KsRAkQOzrjl2CSz9TaGyoU6Iy/DFoQL6hWIzEX8WmhKGLlHOwGYQTbWRbAHiNF23pfsOKQaFfRjiVJ5pImDwFTrisSMcI0xiouEeuwrBnL/HU9y5evJTq0tQz5uzPmjk98DV1C4KW1GTbHDI8pX8BWzJjhPM3mkd60FrWiaU=

Thanks for all the suggestions.

When using proof general in terminal mode (emacs -nw), does someone know how to get the terminal to correctly relay commands like C-c C-RET to proof general/company-coq?

Also, does someone have configuration snippets to register alternate keybindings that work well in terminal mode?

I was hoping to run company-coq over ssh on my phone, and I don't even know whether I need to fix the terminal on my phone or something on the ssh host.

Thanks,

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

On Jan 12, 2017 2:24 PM, "Erik Martin-Dorel" <e.mdorel AT gmail.com> wrote:

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