Commit 2023-06-15 06:25 ec1082a5

View on Github →

chore: move around gcongr material (#5067) Move the gcongr_forward attribute setup from Tactic.GCongr.Core into a new (earlier) file Tactic.GCongr.ForwardAttr, allowing the four seed mini-tactics with this attribute to be moved (earlier) from Tactic.GCongr into Tactic.GCongr.Core. This fixes the broken tests #5065 as well as an issue

I naively assumed that if the tacticgcongr is known, then I would not have to import additional files. So if I import this file, .... gcongr suddenly used a hypothesis where it didn’t do it before. reported by @nomeata .

Estimated changes