`Abort`-ing doesn't clear the goal window (or show the previous current goal) #168

cpitclaudel · 2017-03-08T20:08:56Z

@Matafou Is this another case of the problems we noticed recently? Thanks!

Matafou · 2017-03-08T21:31:34Z

Probably.

axe1d mentioned this issue Mar 31, 2024

Add features: use goal count information printed at top of goals buffer in modeline, clear the goal window when proof is skipped (abort, admitted...). #755

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`Abort`-ing doesn't clear the goal window (or show the previous current goal) #168

`Abort`-ing doesn't clear the goal window (or show the previous current goal) #168

cpitclaudel commented Mar 8, 2017

Matafou commented Mar 8, 2017

Abort-ing doesn't clear the goal window (or show the previous current goal) #168

Abort-ing doesn't clear the goal window (or show the previous current goal) #168

Comments

cpitclaudel commented Mar 8, 2017

Matafou commented Mar 8, 2017

`Abort`-ing doesn't clear the goal window (or show the previous current goal) #168

`Abort`-ing doesn't clear the goal window (or show the previous current goal) #168