coq - The formal proof system

Age	Commit message (Expand)	Author
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-06-09	Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in a	msozeau
2010-06-08	Made option "Automatic Introduction" active by default before too many	herbelin
2010-05-28	Generalized the formulation of classic_set in propositional contexts	herbelin
2010-05-22	Added UIP_dec on suggestion of Eelis on #coq irc.	herbelin
2010-05-09	Added a few informations about file lineages (for the most part in kernel)	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-03-30	Small improvements around coqdoc (including fix for bug #2288)	herbelin
2009-12-09	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey
2009-11-24	Small extra result on JMeq vs eq_dep.	herbelin
2009-11-16	Some lemmas about dependent choice + extensions of Compare_dec +	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-10-27	Add a new vernacular command for controling implicit generalization of	msozeau
2009-10-13	MSets: a new generation of FSets	letouzey
2009-09-28	Fix the stdlib doc compilation + switch all .v file to utf8	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-03	Added "etransitivity".	herbelin
2009-05-27	Stop using a "Manual Implicit Arguments" flag and support them as soon	msozeau
2009-04-28	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin
2009-01-27	- Fixed various Overfull in documentation.	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-12-17	FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...	letouzey
2008-12-16	Move FunctionalExtensionality to Logic/ (someone please check that the	msozeau
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-07-15	Autour du parsing:	herbelin
2008-06-10	- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.	herbelin
2008-04-04	A file that can be loaded when a migration from Set to Type is desired	letouzey
2008-04-04	Correction problème de compil (blast.ml)	herbelin
2008-03-30	Modifications diverses et variées :	herbelin
2008-03-23	Nettoyage Wf.v et unification (suite remarques faites sur cocorico)	herbelin
2008-03-23	Une passe sur les réels:	herbelin
2008-03-04	migration from Set to Type of FSet/FMap + some dependencies...	letouzey
2008-02-02	factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...	letouzey
2008-01-23	Changing R to a local definition so that it isn't exported.	roconnor
2007-11-24	* A few Parameter Inline, but they dont seem to help much concerning	letouzey
2007-10-29	Revision of the FSetWeak Interface, so that it becomes a precise	letouzey
2007-10-03	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin
2007-10-01	Nouvelle mise à jour	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-09-26	added a lemma to prove inj_pair2 when eq_dec is available.	vsiles
2007-06-21	Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,	notin
2007-05-22	Comparaison JMeq/eq_dep	herbelin
2007-04-25	Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création	herbelin
2007-03-15	Typos	herbelin
2007-02-06	Passage de Set à Type dans Relations et Wellfounded	herbelin
2007-01-31	Correction typo eq_rec_eq (cf bug #1339)	herbelin
2007-01-23	Derivation of (exists x : A, P x) -> {x : A \| P x} for decidable P	emakarov
2007-01-22	Clarification redondance Axiome du choix unique/description	herbelin