aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors/VectorDef.v
Commit message (Expand)AuthorAge
* Bugs revealed by playing with contribsGravatar pboutill2012-05-25
* Vectors takes advantage of pattern matching compiler fixupGravatar pboutill2012-05-11
* 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