Commit 2020-08-28 10:25 a08fb2f7
View on Github →feat(tactic/congr): additions to the congr' tactic (#3936)
This PR gives a way to apply ext after congr'.
congr' 3 with x y : 2 is a new notation for congr' 3; ext x y : 2.
New tactic rcongr that recursively keeps applying congr' and ext.
Move congr' and every tactic depending on it from tactic/interactive to a new file tactic/congr.
The original tactic.interactive.congr' is now best called as tactic.congr'.
Other than the tactics congr' and rcongr no tactics have been (essentially) changed.