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
Reported at https://github.com/coq/coq/issues/16335
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).
oh I see there is a similar topic
Last updated: May 28 2023 at 16:30 UTC