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
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: Dec 01 2023 at 07:01 UTC