Axel

Results 3 comments of Axel

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

> The change is nice. A few remarks here and there. 2 questions: > > * should we remove the code that displays this information in the scritpting buffer then?...

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

> The PR should first be cleaned up (useless files, then reduced to one commit imho. I thank you all for taking the time for reviewing my PR (which is...

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

Hi everyone, I modified my feature for Coq-only implementation, moved my functions to the coq subdir, and adapted the modeline update only when PG is instantiated for Coq. My goal...