| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Rename iffT, add some lemmas about tuple and hlist |  Jason Gross | 2016-11-08 |
| | | | | | Some lemmas admitted | ||
| * | Add IffT, some Proper prod lemmas | Jason Gross | 2016-11-07 |
| | | |||
| * | Add Proper prod instance | Jason Gross | 2016-11-07 |
| | | |||
| * | Add eta_expand to Prod.v | Jason Gross | 2016-10-07 |
| | | |||
| * | Make [inversion_{prod,sigma}] stronger |  Jason Gross | 2016-09-05 |
| | | | | | It can now handle paths used in dependent places. | ||
| * | Add path_prod_eta | Jason Gross | 2016-09-03 |
| | | |||
| * | Add prod_beq | Jason Gross | 2016-09-02 |
| | | |||
| * | Rename congrunce_option to inversion_option, add [inversion_prod] | Jason Gross | 2016-08-31 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |