Goto definition doesn't work for record constructors

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

GNU Lesser General Public License v2.1

152 stars 31 forks source link

Open Alizter opened 3 weeks ago

Alizter commented 3 weeks ago

Record A := Build_A { }.

Locate Build_A.
(* Constructor Foo.Build_A *)
About Build_A.

If I do goto-definition on Build_A on line 4, I would expect to be jumped to line 1 but nothing happens.

Other kinds of constructors like in:

Inductive foo := bar.
About bar.

Have the correct behaviour.

ejgallego commented 3 weeks ago

coq/ast.ml needs fixing I think!