Commit 2018-05-20 06:37 741469ab
View on Github →fix(tactic/interactive): make rcases handle nested constructors correctly
The line changed by this commit was wrong because k might contain
further constructors, which also need to be "inverted".
Fixes #56.
- doc(tactic): Internal documentation for rcases
- style(tactic/rcases): eliminate an unused recursive parameter
- style(*): use rcases more