In a proof which I didn't touch, a tactic fails with stack overflow. (len'
in PCUICSpine.expand_lets_k_ctx_subst_id'
)
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