search

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

Ltac, Notation and Tactic Notation doesn't appear in the document overview #632

Open Alizter opened 10 months ago

Alizter commented 10 months ago

Ltac, Notation and Tactic Notation don't appear in the document overview.

ejgallego commented 10 months ago

Indeed we need to add a plugin registration mechanism to Lang.Ast.Info, as we do for hashing and serialization with SerAPI.

This is a lot of very boring work :(

Alizter commented 2 weeks ago

@ejgallego Can we make progress on this now? I seem to recall you did something similar for Rewrite Rule? Is that all that needs to be done? If so, I can take a stab at it.

ejgallego commented 2 weeks ago

For Notation should be easy, just update the coq/ast.ml:make_info function accordingly.

Things that are defined in Ltac are a bit more tricky, you need to handle in that function VernacExtend case.

This requires serlib support as the ast for Ltac and Tactic Notation lives in the ltac plugin.