unable to use in lazyvim on macos
I did the following:
```bash
brew install opam
opam init
opam install ocaml-lsp-server odoc ocamlformat utop merlin
opam user-setup install
eval $(opam env)
opam pin add rocq-prover 9.0.0
opam install rocqide
opam repo add rocq-released https://rocq-prover.org/opam/released
```
In my lazyvim configuration, I have the following plugin:
```lua
return {
{
"whonore/Coqtail",
init = function()
vim.g.loaded_coqtail = 1
vim.g["coqtail#supported"] = 0
end,
},
}
```
Now, when I open a `.v` file, I get syntax highlighting, but when I run :RocqStart, Lazyvim complains that there is no such command. Also, the keybindings you talk about your readme (like e.g. leader cc) do not show up. When I look at what is loaded with command :Lazy, I can see that coqtail is loaded. When I run :help coqtail I get the help for coqtail.
What piece am I missing?
关闭于 2025-07-06 2 条评论