Vadim Zaliva
Vadim Zaliva
When I try to jump to a definition in the local buffer by pressing `M-.` I got this error: "Definition came from this buffer, but precise location is unknown."
Executing `company-coq-diff-unification-error` got the following error "Stack overflow in regexp matcher"
Pressing `M-.` on definition fails with error "company-coq--get-comment-region: Symbol’s function definition is void: coq-find-comment-start"
Consider following source: ``` Section A. Variable x:nat. Lemma Foo {a:nat}: a = 1. Proof. Admitted. End A. Section B. Variable x:nat. Lemma Bar {a:nat}: a = 1. Proof. Admitted....
Minor thing, but when you type "Print" along autocompletes there is no "Instances"
When I use `M-.` it jumps to a definition if it is defined in another file. However it does not work for ones defined in the current file (above current...
Show Obligation Tactic. does not auto-complete. Try typing "Show Obliga"
This is follow up to #65 I found a way to make control-click work under Aquamacs. I am not Elisp hacker, so here is quick and dirty solution which works....
It would be nice to have a ppx extension which would provide a way to use literals. It is clumsy to write things like `Int32.of_string "0xffffffff"`
I have the following dune file which compiles fine from command line with `dune` but not under merlin: ``` (executable (name main) ; workaround for https://github.com/ocaml/dune/issues/3636 (flags (:standard -w -27...