Wolf Honore
Wolf Honore
No, I was just browsing the code and noticed that some work was unnecessarily re-done on each loop. I think it's pretty unlikely that anyone would reach enough retries for...
The problem is tactics are currently only highlighted when they're in a `coqProofBody` region, which looks for a starting delimiter like `Proof` or `Next Obligation`. Without that it's tricky to...
Somewhat related: #43.
When I next get some time I'll experiment with how hard it is to make a best-effort attempt at something like option 2.
I've been following the debugger progress, but I haven't seen the CoqPL talk yet. It's definitely something I'd like to support once I have the magical combination of motivation to...
CoqIDE also seems to be very slow there.
Looking at the debugging logs it seems like it could be because there are a lot of shelved and admitted goals that have fairly large proof contexts so the XML...
This should finally be solvable now with coq/coq#15623.
That's because a line beginning with `*` could either be a bullet or a comment continuation, and I don't know of a way to teach Vim to recognize the difference...
No need to apologize. I made a lot of these decisions a while ago when I was pretty much the only user so I'm glad to get more opinions on...