aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors
Commit message (Expand)AuthorAge
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* drop vo.itarget files and compute the corresponding the corresponding values ...Gravatar Matej Kosik2017-06-01
* Added take to VectorDef.Gravatar George Stelle2017-03-30
* Move vector/list compat notations to their relevant filesGravatar Jason Gross2016-09-29
* Remove spaces from around vector notationsGravatar Jason Gross2016-09-26
* Fix bug #4785 (use [ ] for vector nil)Gravatar Jason Gross2016-09-26
* Fixing bug #4684: Singleton list notation unusable in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-04-25
* 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
* 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
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* 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
* Nicer infered names in refine.Gravatar aspiwack2013-11-04
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Normalized type for Vector.map2Gravatar pboutill2013-03-25
* cbn friendly VectorDefGravatar pboutill2013-02-25
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Same for FinGravatar pboutill2012-07-25
* Vector equalities first stuffGravatar pboutill2012-07-20
* Bugs revealed by playing with contribsGravatar pboutill2012-05-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
* Less ambitious application of a notation for eq_rect. We proposedGravatar herbelin2011-08-10
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
* Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)Gravatar herbelin2011-07-16
* As many notation for for vectors as for List.Gravatar pboutill2011-05-03
* - Fix solve_simpl_eqn which was cheking instances types in the wrong environm...Gravatar msozeau2011-03-23
* Inference of match predicate produces ill-typed unification problem,Gravatar msozeau2011-03-11
* Vectors fully use implicit argumentsGravatar pboutill2011-02-10
* Fixpoints are traverse during implicits arguments search to toplevelGravatar pboutill2011-02-10
* Interp a definition with the implicit arguments of its local contextGravatar pboutill2011-02-10
* local variables can have implicits locallyGravatar 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