coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-12-28	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin
2006-12-12	AllÃègement de syntxe suite à l'introduction de l'unif pattern	herbelin
2006-10-17	Mise en forme des theories	notin
2006-08-28	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-24	JMeq maintenant applicable sur Type	herbelin
2006-07-06	Typo	herbelin
2006-07-04	MAJ du manuel de référence	notin
2006-06-09	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...	herbelin