index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Logic
Commit message (
Expand
)
Author
Age
*
Adding a dependent version of equal_f, thus fixing #3074.
ppedrot
2013-08-02
*
A constructive proof of Fan theorem where paths are represented by predicates.
herbelin
2013-06-02
*
Unset Asymmetric Patterns
pboutill
2013-01-18
*
Making subset_eq_compat applying over more general domain "Type" (see #2938).
herbelin
2012-12-05
*
Identities over types satisfying Uniqueness of Identity Proofs
herbelin
2012-12-04
*
Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing
herbelin
2012-11-15
*
Added a proof that Prop<>Type, for arbitrary fixed Type.
herbelin
2012-11-15
*
A decidability property of functional relations over decidable codomains.
herbelin
2012-11-15
*
For the record, two examples of short proofs of uniqueness of identity
herbelin
2012-11-15
*
Updating headers.
herbelin
2012-08-08
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
2012-07-05
*
ZArith + other : favor the use of modern names instead of compat notations
letouzey
2012-07-05
*
Intuition: temporary(?) restore the unconditional unfolding of not
letouzey
2012-05-15
*
remove undocumented and scarcely-used tactic auto decomp
letouzey
2012-04-23
*
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-11-21
*
Cleaning a little bit the files talking about descriptions: avoiding
herbelin
2011-11-03
*
Removing vernacular code mistakenly committed.
herbelin
2011-10-05
*
Use of the standard terminology for Diaconescu's theorem (not "paradox").
herbelin
2011-08-23
*
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
*
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
*
First release of Vector library.
pboutill
2010-12-10
*
Used multiple lists of implicit arguments to transfer the choices of
herbelin
2010-10-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Made notations for exists, exists! and notations of Utf8.v recursive notations
herbelin
2010-07-22
*
Backported r13308 (ConstructiveEpsilon.v) to branch v8.3
herbelin
2010-07-22
*
Update of ConstructiveEpsilon.v by Jean-François Monin.
herbelin
2010-07-22
*
Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in a
msozeau
2010-06-09
*
Made option "Automatic Introduction" active by default before too many
herbelin
2010-06-08
*
Generalized the formulation of classic_set in propositional contexts
herbelin
2010-05-28
*
Added UIP_dec on suggestion of Eelis on #coq irc.
herbelin
2010-05-22
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Small improvements around coqdoc (including fix for bug #2288)
herbelin
2010-03-30
*
Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...
letouzey
2009-12-09
*
Small extra result on JMeq vs eq_dep.
herbelin
2009-11-24
*
Some lemmas about dependent choice + extensions of Compare_dec +
herbelin
2009-11-16
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Add a new vernacular command for controling implicit generalization of
msozeau
2009-10-27
*
MSets: a new generation of FSets
letouzey
2009-10-13
*
Fix the stdlib doc compilation + switch all .v file to utf8
letouzey
2009-09-28
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Added "etransitivity".
herbelin
2009-08-03
*
Stop using a "Manual Implicit Arguments" flag and support them as soon
msozeau
2009-05-27
*
Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs
herbelin
2009-04-28
*
- Fixed various Overfull in documentation.
herbelin
2009-01-27
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- Optimized "auto decomp" which had a (presumably) exponential in
herbelin
2008-12-26
[next]