aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors/VectorSpec.v
Commit message (Expand)AuthorAge
* Emphasizing that eta for vectors is an instance of caseS, as pointedGravatar Hugo Herbelin2015-09-08
* Adding a proof of eta on Vector.t of non-zero size.Gravatar Hugo Herbelin2015-09-08
* There was one more universe needed due to the use of now non-universe-polymor...Gravatar Matthieu Sozeau2015-01-18
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Vector equalities first stuffGravatar pboutill2012-07-20
* Vector: missing injection lemmas and better impossible branchesGravatar pboutill2012-02-29
* Vectors fully use implicit argumentsGravatar pboutill2011-02-10
* First release of Vector library.Gravatar pboutill2010-12-10