Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Don't rely on autogenerated names | 2017-06-05 | |
| | | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch). | ||
* | Get rid of list-based Tuple.map | 2017-03-30 | |
| | |||
* | Add hlistP | 2016-11-22 | |
| | |||
* | Add rhlist | 2016-11-22 | |
| | |||
* | Add HList.mapt_Proper | 2016-11-17 | |
| | |||
* | prove last HList admit | 2016-11-11 | |
| | |||
* | Add Tuple and HList lemmas | 2016-11-10 | |
| | |||
* | Add hlist_map | 2016-11-08 | |
| | |||
* | Add HList.const | 2016-11-08 | |
| | |||
* | Rename iffT, add some lemmas about tuple and hlist | 2016-11-08 | |
| | | | | Some lemmas admitted | ||
* | Add map_is_mapt' | 2016-11-07 | |
| | |||
* | Add HList lemma | 2016-11-06 | |
| | |||
* | Add admitted lemma about tuple map, add hlist lem | 2016-11-06 | |
| | |||
* | Change hlist implicit status | 2016-11-01 | |
| | |||
* | Move hlist to new file | 2016-11-01 | |