aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Sigma.v
Commit message (Collapse)AuthorAge
* Remove useless hypotheses for [path_sigT_uncurried_iff]Gravatar Jason Gross2016-08-01
| | | | They were breaking tactics
* 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