In a proof which I didn't touch, a tactic fails with stack overflow. (
I presume this is because I added a few lemmas to the
len database, but I feel like I've done something wrong, what could that be ?
What is the tactic?
NB: Changing them to
len seems to work, so it's not a big problem.
Ltac len' := rewrite_strat (topdown (repeat (old_hints len))).
Last updated: Jun 01 2023 at 12:01 UTC