Yann Leray (Dec 07 2022 at 16:19): Yann Leray (Dec 07 2022 at 16:19):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 ?
Théo Winterhalter (Dec 07 2022 at 16:20):What is the tactic?
Yann Leray (Dec 07 2022 at 16:21):NB: Changing them to len seems to work, so it's not a big problem.
Yann Leray (Dec 07 2022 at 16:21):Ltac len' := rewrite_strat (topdown (repeat (old_hints len))).
Last updated: Jun 01 2023 at 12:01 UTC