Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Make Prod.eta_expand also work in the context | 2018-08-10 | |
* | Revert "Add more schemes for prod" | 2018-06-28 | |
* | Add more schemes for prod | 2018-06-28 | |
* | Add subst_prod tactic to Prod.v | 2017-05-19 | |
* | Merge new base system (#112) | 2017-02-22 | |
* | Rename iffT, add some lemmas about tuple and hlist | 2016-11-08 | |
* | Add IffT, some Proper prod lemmas | 2016-11-07 | |
* | Add Proper prod instance | 2016-11-07 | |
* | Add eta_expand to Prod.v | 2016-10-07 | |
* | Make [inversion_{prod,sigma}] stronger | 2016-09-05 | |
* | Add path_prod_eta | 2016-09-03 | |
* | Add prod_beq | 2016-09-02 | |
* | Rename congrunce_option to inversion_option, add [inversion_prod] | 2016-08-31 |