Jason Gross

> It auto generalizes [...] Therefore it can't be better than linear in size of context. @SkySkimmer But there are no indices and the hypothesis being destructed is free in...

The last one. But I'm also trying to destruct the last one. Perhaps `destruct` should have the same optimization that `clear` does for not checking hypotheses that come before the...

Btw, there's a separate issue open for the performance bottlenecks in `intros`: https://github.com/coq/coq/issues/8244

Why is it that `Optimize Proof` speeds up `Qed`, but only a little? Is `Qed` not doing `nf_evar`? Edit: I can't reproduce this behavior

> I did not benchmark Qed because of #8236 but it seemed negligible after `Optimize Proof`, and approximately as slow as `Optimize Proof` without prior `Optimize Proof`. Here are Qed...

@ppedrot Is there any hope of replacing `intros` with a tactic that has the same semantics as `intros` currently does, but is asymptotically faster? It's pretty easy to make a...

Oops, misclick. I'd also be fine with having an `intros` that was fast only in places where you give it an unknown number of introductions. I.e., `intros` without any argument...

> Working on that. Thanks! > The only tradeoff is in terms of compacity, and it does seem to have a mild influence on degenerate cases from mathcomp, although I...

> So I have a version of intros that does batch evar creation, but it turns out that there are other places that are quadratic in the number of context...

Any updates on this @ppedrot ?