Pierre Courtieu

Results 266 comments of Pierre Courtieu

Unexpected behaviour of specialize with (...:=...) in combination with typeclasses

Now that #18341 is abandoned this needs some independent fix.

Fail output not shown when running completely silent

I think the situation is the following (@hendriktews correct me if necessary): 1. For now and for coq

Fail output not shown when running completely silent

> No. IMO for 9.2 we need to make `Set Silent` in `coq-shell-init-cmd` version dependent and disable it for Rocq >= 9.2. That is what I call "what we have...

Fail output not shown when running completely silent

Thanks for proposing. That would be great. @hendriktews what do you think?

Proof General may be forced to run Rocq completely silent for Rocq 9.2

@hendriktews now that the `-emacs` option does not print goals, we don't need the `Set Silent` anymore do we?

Proof General may be forced to run Rocq completely silent for Rocq 9.2

Of course I mean when the next Rocq is detected.