coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq IDE with jump to definition
Date: Thu, 12 Jan 2017 19:46:06 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:5QPDqxKdhHm/d+JZJ9mcpTZWNBhigK39O0sv0rFitYgRKvTxwZ3uMQTl6Ol3ixeRBMOAuq4C0LKd6vq8EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oIhi6sQrdutQIjYZtN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqxbrhy/uhJxwIDUb46JO/VjfKzSc8gXRXZdUstLSyBNHpmxY5UJAuEcPehYtY79p14WoBWxAwmsHuLvxSNPhnTrw6M1yf8hERrH3Ac9GN8BrnLUrM/0NKgOVuC51rXIwi/Yb/NN2Dfw84nIchY7ofGNR718a8TRyVM2Gg7Dk16eqpTlMiuR2+kCqWSX8eRtWfiuhmMjsQ19vyajy8U0hoXUmo4YzkrI+CtkzIovONG1TE12bcSgHZZWqiqULZF5Qtk4TGFtoCs6yqMJuZq8fCUSxpQo2QLfa+Cac4iO/hLsTvydITBihHJqYL6/hhCy/la8yuDkUsS530xGojRLn9XWt30A0wbf5tWZRvZ/5kuh3CyA1wHX6uFKO0A0kq/bJoYuwrEqjJocr1/DEzT4mErokK+Walgk+u606+v9eLnmoYWcN4BshgHkLqsugtC/Afg/MgUWQ2eb/v282KT/8k39XbVFleY7krLZsZDfPcQUvLS1Aw5T0oY56hawFS2q0NoCnSpPEFUQcxWeyoPtJlvmIfbiDP75jU7/vi1swqXrOKfgCZKFEnHYi7apKbt78U9Xz0wvxMtE5rpVDKsAKbT9QBmi55TjEhYlPlnskK7cA9Jn29ZGVA==

On Thu, Jan 12, 2017 at 12:03:28PM -0500, Abhishek Anand wrote:
> Is there a Coq IDE that does "jump to definition", like the way merlin
> based OCaml IDEs do?

Coqoon does (F3 IIRC).

Best,
--
Enrico Tassi

[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