Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Update headers following #6543. | 2018-02-27 | |
* | Added take to VectorDef. | 2017-03-30 | |
* | Emphasizing that eta for vectors is an instance of caseS, as pointed | 2015-09-08 | |
* | Adding a proof of eta on Vector.t of non-zero size. | 2015-09-08 | |
* | There was one more universe needed due to the use of now non-universe-polymor... | 2015-01-18 | |
* | This commit adds full universe polymorphism and fast projections to Coq. | 2014-05-06 | |
* | Nicer infered names in refine. | 2013-11-04 | |
* | A whole new implemenation of the refine tactic. | 2013-11-02 | |
* | Vector equalities first stuff | 2012-07-20 | |
* | Vector: missing injection lemmas and better impossible branches | 2012-02-29 | |
* | Vectors fully use implicit arguments | 2011-02-10 | |
* | First release of Vector library. | 2010-12-10 |