ITADN

unable to use in lazyvim on macos

#393Closedzadigus 创建于 2025-07-04
Z
zadiguscommented
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 条评论