aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/InversionSigma.v
AgeCommit message (Collapse)Author
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add an [inversion_sigma] tacticJason Gross
This tactic does better than [inversion] at sigma types.