Jonathan Leivent

I have noticed this lag, too - and it is annoying enough that I turn off Company-Coq mode at times just to eliminate it. If you can't easily eliminate it,...

Nice idea. Remember to look for core and use nocore if no core hints are used! Also, it's not just intuition - the other tactics that are implicitly "auto with...

Can company-coq detect when there are remain goals, but none are in focus? If so, then if "-" is bound to an electric bullet in that case but self-insert otherwise,...

This is the tactic (minlines) I use to minimize the lines in a goal: ``` Ltac revert_all := repeat lazymatch goal with H:_ |- _ => revert H end. Ltac...

I just loaded highlight-symbol-mode - thanks for that, it saves on the regexp search. I notice that it doesn't work across panes/frames/windows - so I still have to move the...

Love it! Can it refine the diff down to words?

The obvious case where this is a big help is when a tactic like inversion impacts hypotheses that one didn't anticipate. But, this is also going to make it easier...

I just tried it out, and it is not cooperating in my proofs as nicely as in your demo. I will send along some screen shots...

Here's one: 

Here's another: