I'm trying to profile a tactic in which invocations to `set (x := ..) in *`

are responsible for a good portion of the running time. Is there a faster version of this tactic somewhere that I should use instead, or is what I'm trying to do intrinsically expensive?

`set`

is modulo conversion, see also https://github.com/coq/coq/issues/4636 and https://github.com/coq/coq/issues/13788#issuecomment-767217443 (there's a `fast_set`

in the next comment in https://github.com/coq/coq/issues/13788#issuecomment-767217670). You can speed things up by replacing `set`

with `pose`

and `change`

Thanks a lot! I'm testing your `fast_set`

right now, it looks like it should be a lot better already.

You mention in the issue that an Ltac2 implementation might be even more efficient; if you have such an implementation then I'd also be interested :-).

Last updated: Oct 04 2023 at 20:01 UTC