aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors/Fin.v
Commit message (Expand)AuthorAge
* Simplified rect2, it turns out Arthur's trick was not required.Gravatar Maxime Dénès2014-07-22
* A version of Fin.rect2 that is compatible with the fix of the guard condition.Gravatar Maxime Dénès2014-07-22
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* fixup complement FinGravatar Pierre Boutillier2014-02-24
* FinFun.v: results about injective/surjective/bijective fonctions over finite ...Gravatar Pierre Letouzey2014-02-07
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Same for FinGravatar pboutill2012-07-25
* Vectors takes advantage of pattern matching compiler fixupGravatar pboutill2012-05-11
* Coqide highligthing is back (done by gtksourceview).Gravatar pboutill2012-05-02
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* Vector: missing injection lemmas and better impossible branchesGravatar pboutill2012-02-29
* Vectors use a bit more the pattern matching compilerGravatar pboutill2011-12-07
* VectorDef.v takes benefit of dependencies being taken into accountGravatar herbelin2011-11-21
* Vectors fully use implicit argumentsGravatar pboutill2011-02-10
* Interp a definition with the implicit arguments of its local contextGravatar pboutill2011-02-10
* Data structure telling implicits of local variables is a map in theGravatar pboutill2011-02-10
* First release of Vector library.Gravatar pboutill2010-12-10