mathlib3
d9476d44 - fix(tactic/rcases): Don't parameterize parsers (#9159)

Commit
4 years ago
fix(tactic/rcases): Don't parameterize parsers (#9159) The parser description generator only unfolds parser constants if they have no arguments, which means that parsers like `rcases_patt_parse tt` and `rcases_patt_parse ff` don't generate descriptions even though they have a `with_desc` clause. We fix this by naming the parsers separately. Fixes #9158
Author
Parents
Loading