aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Sigma.v
Commit message (Expand)AuthorAge
* Remove useless hypotheses for [path_sigT_uncurried_iff]Gravatar Jason Gross2016-08-01
* Add inversion helper tactics to Sigma.vGravatar Jason Gross2016-07-29
* Rename path_sig{,T}{ => _uncurried}_iffGravatar Jason Gross2016-07-29
* Add path_sig{,T}_iffGravatar Jason Gross2016-07-29
* Add some lemmas to Util.SigmaGravatar Jason Gross2016-07-29
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29