search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
145 stars 31 forks source link

Adding definition kind LetContext #654

Closed herbelin closed 5 months ago

herbelin commented 6 months ago

This is in anticipation of coq/coq#13445 which introduces a new declaration LetContext for referring to local definitions introduced by Context (while, beforehand, it was using Definition). I however wonder whether this is maybe overkell: an alternative would be to use Letas we do for local definiitions, renouncing to make a difference between Let x:=t and Context (x:=t).

proux01 commented 5 months ago

Upstream PR merged, please merge

ejgallego commented 5 months ago

Will merge as soon as CI passes.

We always require the CI to pass before a merge here, and we have deterministic builds, so usually bumping the Coq submodule is necessary before merge, as I've just done.