Commit 2022-02-09 13:22 226f899c

feat: rcases and rintro tactics (#182) I finally got around to porting rcases for real. There are a few things that should probably be upstreamed: generalizeExceptFVar is a piece of a function in cases, and FVarSubst.append does not belong here. Indeed FVarSubst.append is only needed because cases does not expose a FVarSubst argument even though it talks about having one in the comments. obtain, rcases, and rintro are fully implemented, but rcases? and rintro? have not been implemented yet; I intend to do these in a follow up PR.