Pierre Courtieu

> @Matafou : I would like to repeat to ensure I understand: When fine tuning type classes, you assert bigger chunks (so Coq is switch to silent), in these chunks...

> * keep the error message visible and only update the goals buffer in the background Maybe the simplest is to store the error message and re-insert it afterward? >...

@hendriktews I am playing with your version and it seems to work quite well. > This is my first partial take on issue #188 and Pierre's example in PR #429...

OK I will try to make something from your PR. I never did this before, do I just push directly on your branch?

OK thanks. Currently your branch falls into a loop if an error occurs when not in a proof (Show sends an error which triggers the same piece of code again,...

This should work correctly now. - I had to first commit https://github.com/ProofGeneral/PG/commit/5807535598911346f09db0091ccbb2d1c3283433 to have the information about being in proof mode at this point of the code. - There are...

> * To fix this correctly I need to figure out how to detect that no goal were displayed since the beginning of the bunch. Or maybe just check the...

by the way @erikmd @CyrilAnac my previous force-push had a spurious debug message left in the code and it made the CI test fail apparently, which is fine, but when...

I forced pushed a commit and it solved the problem, if I have time I will try to understand why the test took so long. It cannot be just because...

I will. But I think I know the problem. There was indeed a loop in some cases in Hendrik's first try, and my force push did not fix it yet.