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
gcongr
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 .