index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-11-21
*
VectorDef.v takes benefit of dependencies being taken into account
herbelin
2011-11-21
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
Cleaning a little bit the files talking about descriptions: avoiding
herbelin
2011-11-03
*
Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).
herbelin
2011-10-26
*
Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).
herbelin
2011-10-25
*
Fixing Equality.injectable which did not detect an equality without
herbelin
2011-10-22
*
Fix bug #2586 and enhance clsubst* as well as a side effect
msozeau
2011-10-18
*
Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...
msozeau
2011-10-17
*
MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right
letouzey
2011-10-14
*
Proper fix for complement/flip instances.
msozeau
2011-10-10
*
fsetdec : non-atomic elements are now transformed as variables first (fix #2464)
letouzey
2011-10-07
*
Fix bug #2557 and an issue with Propers for complement
msozeau
2011-10-07
*
Improved handling of element equalities in fsetdec (fix #2467)
letouzey
2011-10-07
*
Removing vernacular code mistakenly committed.
herbelin
2011-10-05
*
Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...
letouzey
2011-10-05
*
Moving never-used comments from Zhints.v to dev/doc so as not to
herbelin
2011-10-01
*
Euclid: make the proof transparent (example of extraction in stdlib)
letouzey
2011-09-17
*
Omega: for non-arithmetical goals, try proving False from context (wish #2236)
letouzey
2011-09-16
*
Avoid registering λ and Π as keywords just for some private Local Notation
letouzey
2011-09-06
*
Bug 2589: Documentation patch of Hendrik Tews
pboutill
2011-09-02
*
Use of the standard terminology for Diaconescu's theorem (not "paradox").
herbelin
2011-08-23
*
Give inner fixpoint of gcd31 a name, to avoid excessive unfolding
glondu
2011-08-17
*
Smaller proof terms for QcPower_{0,pos}
glondu
2011-08-17
*
SearchAbout and similar: add a customizable blacklist
letouzey
2011-08-11
*
Take benefit of bullets available by default in Prelude
herbelin
2011-08-10
*
Less ambitious application of a notation for eq_rect. We proposed
herbelin
2011-08-10
*
BinInt: more structured scripts thanks to bullets and { }
letouzey
2011-08-09
*
Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...
aspiwack
2011-08-09
*
Some forgotten lemma in Arith with "O" in the name instead of "0".
herbelin
2011-08-08
*
New proposition "rewrite Heq in H" for eq_rect (assuming that there is
herbelin
2011-08-08
*
All the parameters of Compare are implicits.
pboutill
2011-07-26
*
All the parameters of or can be implicits.
pboutill
2011-07-26
*
Same Implicit Arguments rule for sumbool and sumor.
pboutill
2011-07-26
*
Some facts about functional extensionality (especially alternative
herbelin
2011-07-16
*
More lemmas relating the different equivalent formulations of eq_dep.
herbelin
2011-07-16
*
Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)
herbelin
2011-07-16
*
Added a characterization of unique existence.
herbelin
2011-07-16
*
StrictOrder marked explicitly to be in Prop
letouzey
2011-07-04
*
Some cleanup of Zcomplements
letouzey
2011-07-01
*
Cleanup of files related with power over Z.
letouzey
2011-07-01
*
Cleanup in SpecViaZ
letouzey
2011-06-30
*
Cleanup of Ndigits
letouzey
2011-06-30
*
Deletion of useless Zdigits_def
letouzey
2011-06-28
*
Deletion of useless Zlog_def
letouzey
2011-06-28
*
Deletion of useless Zsqrt_def
letouzey
2011-06-28
*
Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def
letouzey
2011-06-28
*
Some cleanup of Wf_Z.v
letouzey
2011-06-28
*
Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)
letouzey
2011-06-27
*
Znumtheory: a correct version of a compatibility Zdivide_intro
letouzey
2011-06-27
[next]