Stream: Coq devs & plugin devs

Topic: Error: Anomaly "Stm.join: tip not cached"

Jason Gross (Jul 20 2022 at 17:56):

What does Error: Anomaly "Stm.join: tip not cached" mean? It seems to lack a location and be very sensitive to which commit of Coq I'm running

Jason Gross (Jul 20 2022 at 18:37):

Reported at https://github.com/coq/coq/issues/16335

Ali Caglayan (Sep 28 2022 at 21:36):

What does this usually indicate?

Error: Anomaly "Stm.join: tip not cached"

I got it removing ln 119 of plugins/ltac/g_rewrite.mlg and running

Require Import Setoids.Setoid.
Inductive I := Foo | Bar.
Parameter Hyp : forall n : nat, (Foo = Bar) <-> True.
Goal Foo = Bar. rewrite_strat (Hyp 0).

Ali Caglayan (Sep 28 2022 at 21:36):

oh I see there is a similar topic

Last updated: Dec 01 2023 at 07:01 UTC