index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Vectors
/
Fin.v
Commit message (
Expand
)
Author
Age
*
fixup complement Fin
Pierre Boutillier
2014-02-24
*
FinFun.v: results about injective/surjective/bijective fonctions over finite ...
Pierre Letouzey
2014-02-07
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Same for Fin
pboutill
2012-07-25
*
Vectors takes advantage of pattern matching compiler fixup
pboutill
2012-05-11
*
Coqide highligthing is back (done by gtksourceview).
pboutill
2012-05-02
*
Remove support for "abstract typing constraints" that requires unicity of sol...
msozeau
2012-03-14
*
Vector: missing injection lemmas and better impossible branches
pboutill
2012-02-29
*
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
*
Vectors fully use implicit arguments
pboutill
2011-02-10
*
Interp a definition with the implicit arguments of its local context
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