proof as you go

[czhang03]

give an option to invoke proofs when you type - or ., so that we don't need to C-c C-ent every time

[siegebell]

proposed option: "coq.autoAdvanceFocus": true Causes the focus to advance forward when the user completes a sentence (types ., followed by a whitespace character (space, tab, or newline; not a comment), and when correctly bracketed) and the focus is at the beginning of the sentence being completed. In result, the completed sentence will be sent to coqtop for processing and the focus will advance to the end of the sentence.

[siegebell]

@chantisnake when & why would you want the focus to advance in response to -? Is it because it is a bullet?

[czhang03]

Right...

[siegebell]

ok then.

I'll include all the bullets: *+-{}

[czhang03]

Thank you!