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 tactic
gcongris known, then I would not have to import additional files. So if I import this file, ....gcongrsuddenly used a hypothesis where it didn’t do it before. reported by @nomeata .