coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...	letouzey	2008-12-17
*	Move FunctionalExtensionality to Logic/ (someone please check that the	msozeau	2008-12-16
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Autour du parsing:	herbelin	2008-07-15
*	- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.	herbelin	2008-06-10
*	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-04-04
*	Modifications diverses et variées :	herbelin	2008-03-30
*	Nettoyage Wf.v et unification (suite remarques faites sur cocorico)	herbelin	2008-03-23
*	Une passe sur les réels:	herbelin	2008-03-23
*	migration from Set to Type of FSet/FMap + some dependencies...	letouzey	2008-03-04
*	factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...	letouzey	2008-02-02
*	Changing R to a local definition so that it isn't exported.	roconnor	2008-01-23
*	* A few Parameter Inline, but they dont seem to help much concerning	letouzey	2007-11-24
*	Revision of the FSetWeak Interface, so that it becomes a precise	letouzey	2007-10-29
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Nouvelle mise à jour	herbelin	2007-10-01
*	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin	2007-09-30
*	added a lemma to prove inj_pair2 when eq_dec is available.	vsiles	2007-09-26
*	Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc,	notin	2007-06-21
*	Comparaison JMeq/eq_dep	herbelin	2007-05-22
*	Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création	herbelin	2007-04-25
*	Typos	herbelin	2007-03-15
*	Passage de Set à Type dans Relations et Wellfounded	herbelin	2007-02-06
*	Correction typo eq_rec_eq (cf bug #1339)	herbelin	2007-01-31
*	Derivation of (exists x : A, P x) -> {x : A \| P x} for decidable P	emakarov	2007-01-23
*	Clarification redondance Axiome du choix unique/description	herbelin	2007-01-22
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
*	AllÃègement de syntxe suite à l'introduction de l'unif pattern	herbelin	2006-12-12
*	Mise en forme des theories	notin	2006-10-17
*	Passage à une définition de inhabited plus dans les 'standard mathématique...	herbelin	2006-08-28
*	"Essai de remplacement de "ex P" par "exists x, P x" suite à	herbelin	2006-08-28
*	JMeq maintenant applicable sur Type	herbelin	2006-08-24
*	Typo	herbelin	2006-07-06
*	MAJ du manuel de référence	notin	2006-07-04
*	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...	herbelin	2006-06-09
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
*	Ajout exists! et restructuration/extension des fichiers sur la	herbelin	2006-06-04
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Réajout de eq_rec_eq oublié lors de la modularisation de Eqdep	herbelin	2006-03-30
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05
*	Commentaires	herbelin	2006-03-05
*	Renommage du IP classique pour éviter confusion avec IP constructif	herbelin	2006-03-05
*	Ajout étude IP généralisé, Gödel-Dummett, buveur	herbelin	2006-03-05
*	Petite simplification en passant	herbelin	2006-03-04
*	add a left and right tactic for classical logic	narboux	2005-07-15