Pierre Courtieu
Pierre Courtieu
> But as I had mentioned in another comment, do you think `by rewrite lem1 lem2; last apply: lem3.` would admit a proper expansion? Maybe something like: ```coq { all:...
I guess we won't work on a poc until summer holidays. By the way, looking back at the first example of this feature wish:. ```coq by rewrite leqNgt (leq_trans m_gt1)...
Good point. IMHO the idea is either you have a _CoqProject file either you set `coq-prog-args` because implicitly `coq-prog-args` is mainly for setting the load-path. For user options you should...
Indeed it is a bit rough at the edges. We need to make this easier to set up. Especially because dune is also coming in the game and we probably...
Agreed, this needs a proper and documented solution.
Do we want to merge this as is? IS there something more to do? Concerning toolbar icons this could be done in another PR.
FTR: - slowlyness was solved by @hendriktews (reusing tramp connexion) - the bug which triggers some assertion is still there as far as we can tell. Merging now would need...
Yes, this seems to be a missing in ltac2 messages. I will fill a bug report in Coq. That said the given script gives an error in coq v8.11 and...
OK it works in v8.13. Workaround: ``` Ltac2 rec wait2(n: int) := let _ := ltac1:(idtac "hi") in Control.time None (fun _ => if Int.equal n 0 then () else...
The workaround is not very satisfying as a real solution. The reason of Set Silent/Unset Silent. is performance. If you go trough a big script showing all the intermediate goals...