Vincent
Vincent
It looks like the discussion hit a dead end last year. Do you think with some external use cases we could get new traction on that direction ? It looks...
By the way, it really looks like ejgallego/coq-lsp#331, so feel free to close and move the discussion there
Since it's still open, I'm taking the opportunity to ask an implementation question: in https://github.com/vsiles/coq-serapi/commit/e456953a3ab57f4a23c623729c3137e9e0317ece I quickly hacked what I think could be the "notation erasure" function. As you can...
> > Does that ring any bell ? > > Umm, it seems you are using an incomplete build? Does it work if you do `dune build` before? So I...
got it running fine with dune, thanks !
@ejgallego Ok, my attempt seems to work "kind of"... but there's some cases where it doesn't work at all (involving inductive types e.g., not sure what's wrong). What would be...
Is there any progress on that front, or can I help in some ways ?
In case it helped, I tried to use `:set verbose=15` and I'm seeing some `Exception caught: Vim(return):E121: Undefined variable: b:coqtail_panel_bufs`, or this ``` chdir(/Users/vsiles/.vim/bundle/Coqtail/autoload/coqtail) fchdir() to previous dir line 15:...
In case of doubt, reboot... Now things looks ok. I'll monitor this today. Please tell me if anything in the log looks suspicious
No problem today either. I really feel something was wrong with my mac and reboot fixed it. I did tried to do `CoqToggleDebug` but I didn't see much. Where is...