ejgallego / coq-lsp

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

[plugin] Debug plugin for printing universe deltas in files. #773

Closed ejgallego closed 1 month ago

ejgallego commented 1 month ago

Can be used with:

$ dune exec -- fcc --root $absolute_path --max_errors=0 --plugin=coq-lsp.plugin.univdiff $absolute_path.v
$ cat $absolute_path.v.univdiff

cc: #310