index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Vectors
Commit message (
Expand
)
Author
Age
*
Vectors use a bit more the pattern matching compiler
pboutill
2011-12-07
*
VectorDef.v takes benefit of dependencies being taken into account
herbelin
2011-11-21
*
Less ambitious application of a notation for eq_rect. We proposed
herbelin
2011-08-10
*
New proposition "rewrite Heq in H" for eq_rect (assuming that there is
herbelin
2011-08-08
*
Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)
herbelin
2011-07-16
*
As many notation for for vectors as for List.
pboutill
2011-05-03
*
- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...
msozeau
2011-03-23
*
Inference of match predicate produces ill-typed unification problem,
msozeau
2011-03-11
*
Vectors fully use implicit arguments
pboutill
2011-02-10
*
Fixpoints are traverse during implicits arguments search to toplevel
pboutill
2011-02-10
*
Interp a definition with the implicit arguments of its local context
pboutill
2011-02-10
*
local variables can have implicits locally
pboutill
2011-02-10
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
First release of Vector library.
pboutill
2010-12-10