The Coq mailing list

[Hans Jacob Fehrmann Rojas <hans.jfehrmann AT gmail.com>]

Thanks. This was the solution.

Hans.

On Sat, Apr 21, 2018 at 1:58 PM, Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

Note that with Coq master -debug is on by default and -annotate is now -bin-annot.

Also, there is a Merlin file in the Coq sources.

Le sam. 21 avr. 2018 à 18:44, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

There's probably a better way to do this, but here's what I do for plugin work:

I manually build coq (the same version as that of the coq binaries) from sources, say in a directory X.

While building Coq, I pass the following options to ./configure: -debug -annotate

Then, in ~/.merlin, I add the following:

FLG -rectypes

B X/config

B X/lib

B X/intf

B X/kernel

B X/kernel/byterun

B X/library

B X/engine

B X/pretyping

B X/interp

B X/proofs

B X/tactics

B X/printing

B X/parsing

B X/toplevel

B X/tools

B X/tools/coqdoc

B X/dev

B X/stm

B X/plugins/ltac

B X/vernac

Then, in vscode, I am able to jump (to definition) around in Coq sources and see types of items that are in Coq sources.

On Sat, Apr 21, 2018 at 11:33 AM Hans Jacob Fehrmann Rojas <hans.jfehrmann AT gmail.com> wrote:

I am developing a plugin in emacs with merlin. Today I changed my pc and now I am not able to locate the function on the coq modules. The problem seems to be some cmt files missing. How can this be fixed?

Best,

Hans.

--

-- Abhishek

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