Commit 2023-04-18 03:36 83fa5548
View on Github →feat: with clauses for congr!/convert/convert_to (#3060)
Adds with clauses to congr! and friends consisting of a list of rintro patterns. These patterns are used when these tactics intro variables.