Stream: MetaCoq

Topic: Stack overflow during a tactic


view this post on Zulip 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 ?

view this post on Zulip Théo Winterhalter (Dec 07 2022 at 16:20):

What is the tactic?

view this post on Zulip Yann Leray (Dec 07 2022 at 16:21):

NB: Changing them to len seems to work, so it's not a big problem.

view this post on Zulip Yann Leray (Dec 07 2022 at 16:21):

Ltac len' := rewrite_strat (topdown (repeat (old_hints len))).

Last updated: Feb 04 2023 at 02:03 UTC