aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
Commit message (Expand)AuthorAge
* Add some move/transport eq lemmasGravatar Jason Gross2019-04-22
* Add push_rew_fun_depGravatar Jason Gross2019-04-22
* Add PrimitiveSigmaGravatar Jason Gross2018-09-14
* Minor refactoringGravatar Jason Gross2018-06-13
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Add ap_transport to Equality.vGravatar Jason Gross2017-04-02
* Add match commutation lemmasGravatar Jason Gross2017-01-23
* Minor additionsGravatar Jason Gross2017-01-23
* Util.Equality on 8.4Gravatar Andres Erbsen2016-08-04
* Add documentation: Equality, HProp, Isomorphism, Sigma (#41)Gravatar Jason Gross2016-08-01
* Fixes for Coq 8.4Gravatar Jason Gross2016-08-01
* Add a lemma about hprop and eqGravatar Jason Gross2016-07-29
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29