Pierre Courtieu
Pierre Courtieu
> @Matafou I'm open to experimentation, but I'm somewhat wary that the ssr people have already an equivalent feature for the high-level variant. IIRC there is an extremely similar mechanism...
Hi. We welcome such contributions! Of course the maintenance of this code remains yours. We generally proceed by PR. I would recommend (although this is not a prerequisite) that you...
But an immediate PR of your current fork would be welcome. Please be patient we will look at it when we have time (we all do this in our spare...
This sounds like a good idea, althoug in other provers (like coq) the indentation of proof script is better done using script structure itself, i.e. script bulleting and parenthesizing. Like...
Looks like compilation messages. Probably the first time some file is loaded triggers it's compilation. @hendriktews any idea?
@RalfJung Please let us know if this solved the annoyance. @monnier is there something else we can do except fix each and every warning in the code?
OK let us have this on our todo list then. I suspect in 6 months everybody will have switched to emacs 28 so we should at least reduce the warnings...
Indeed thx for reporting!
I will try to build a list when I have some time. The things I see right now are Print Check About Search... Time Show Focus (edited) I see a...