Commit 2021-01-03 23:18 4fcf65c0
View on Github →fix(tactic/rcases): fix rcases? goal alignment (#5576)
This fixes a bug in which rcases? will not align the goals correctly
in the same manner as rcases, leading to a situation where the hint
produced by rcases? does not work in rcases.
Also fixes a bug where missing names will be printed as [anonymous]
instead of _.
Fixes #2794