Pierre Courtieu
Pierre Courtieu
Hi! Nice to have feedback! > Hi @Matafou > > Thanks for your work on the new indentation engine! Here are a few things that could be improved. > >...
> These 3 cases are the same problem Sorry only the last case (`(forallx,\n x = x)` is about boxed style. The others should be easy to fix.
I don't see this behaviour. If the line "Context" is shifted then so are the others.
```coq Instance spec_of_upstr : spec_of "upstr" := fnspec! "upstr" s_ptr wlen / (s : list byte) R, { requires tr mem := wlen = word.of_Z (Z.of_nat (length s)); ensures tr'...
Indeed the timing information is present in the *coq* buffer but it is not dispatched in response buffer. Probably because it is not enclosed inside a `` tag. I guess...
Thanks Hendriks! My experiments on the silent stuff date back to more than a decade, maybe two. It was mostly dependent on the size of goals (times the number of...
@cpitclaudel what you guessed is not true currently, but I think we wan tto switch to it (unless async comes to maturity meanwhile). @hendriktews > - keep the error message...
If the last successful command takes long this may feel frustrating.
It is quite common to have a single command taking several seconds. P. Le lun. 13 avr. 2020 à 14:39, hendriktews a écrit : > If the last successful command...
Actually it is generally *more* frequent during proof development, while e.g. type classes have not yet been fine tuned for your purpose.