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
*
Bugs revealed by playing with contribs
pboutill
2012-05-25
*
Permutation: remove a compatibility notation which doesn't help MathClasses
letouzey
2012-05-22
*
SetoidList: explicit the fact that InfA_compat won't use ltA_strorder
letouzey
2012-05-22
*
List + Permutation : more results about nth_error and nth
letouzey
2012-05-18
*
Intuition: temporary(?) restore the unconditional unfolding of not
letouzey
2012-05-15
*
Vectors takes advantage of pattern matching compiler fixup
pboutill
2012-05-11
*
Bug 2767
pboutill
2012-05-09
*
Coqide highligthing is back (done by gtksourceview).
pboutill
2012-05-02
*
A notion of permutation for lists modulo a setoid equality
letouzey
2012-05-02
*
remove undocumented and scarcely-used tactic auto decomp
letouzey
2012-04-23
*
Remove the Dp plugin.
gmelquio
2012-04-17
*
Fixing typo in previous commit r15180.
herbelin
2012-04-15
*
Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).
herbelin
2012-04-15
*
MSetRBT : implementation of MSets via Red-Black trees
letouzey
2012-04-13
*
Uniformisation in the documentation: remove the use of 'coinductive' in
aspiwack
2012-04-13
*
"A -> B" is a notation for "forall _ : A, B".
pboutill
2012-04-12
*
Fixing a few bugs (see #2571) related to interpretation of multiple binders
herbelin
2012-04-06
*
Fixing printing level of Utf8 equivalent for ->.
herbelin
2012-03-26
*
Fix interface of resolve_typeclasses: onlyargs -> with_goals:
msozeau
2012-03-20
*
Turning proofs of well-ordering of lexicographic product transparent
herbelin
2012-03-20
*
Fix bugs related to Program integration.
msozeau
2012-03-19
*
Final part of moving Program code inside the main code. Adapted add_definitio...
msozeau
2012-03-14
*
Everything compiles again.
msozeau
2012-03-14
*
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
*
Fix unblocking code in dependent destruction due to zeta being used in unfold...
msozeau
2012-02-01
*
Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...
msozeau
2012-01-31
*
Tentative to fix bug #2628 by not letting intuition break records. Might be t...
msozeau
2012-01-28
*
Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...
msozeau
2012-01-28
*
Deleted the only use of BeginSubProof from the standard library.
ppedrot
2012-01-23
*
No more use of tauto in Init/
pboutill
2012-01-19
*
MSetAVL: better implementation of filter suggested by X. Leroy
letouzey
2012-01-17
*
Added the decidability of (<=) on nat.
ppedrot
2012-01-13
*
Fixed the itarget of the previous commit...
ppedrot
2012-01-06
*
Added a typeclass-based system to reason on decidable propositions.
ppedrot
2012-01-06
*
Granted legitimate wish #2607 (not exposing crude fixpoint body of
herbelin
2011-12-18
*
Vectors use a bit more the pattern matching compiler
pboutill
2011-12-07
*
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
[next]