| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Make Prod.eta_expand also work in the context |  Jason Gross | 2018-08-10 |
| * | Revert "Add more schemes for prod" | Jason Gross | 2018-06-28 |
| * | Add more schemes for prod | Jason Gross | 2018-06-28 |
| * | Add subst_prod tactic to Prod.v |  Jason Gross | 2017-05-19 |
| * | Merge new base system (#112) |  jadephilipoom | 2017-02-22 |
| * | Rename iffT, add some lemmas about tuple and hlist | Jason Gross | 2016-11-08 |
| * | 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 |
| * | 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 |