coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Big reorganization of romega/ReflOmegaCore.v: towards a modular	letouzey	2007-07-10
*	Extension of NArith: Nminus, Nmin, etc	letouzey	2007-06-07
*	simplier version of tail_plus	letouzey	2007-04-06
*	Proof simplification for eq_nat_dec et le_lt_dec: induction over	letouzey	2007-03-12
*	Ajouts de lemmes dans Min et Max	notin	2007-02-19
*	fixes PR#1269 about function: there is no reason well founded induction is	bertot	2006-11-05
*	simplif de la partie ML de ring/field	barras	2006-10-27
*	Mise en forme des theories	notin	2006-10-17
*	Ajout du théorème mult_minus_distr_l	notin	2006-10-13
*	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras	2006-10-05
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Un gros coup de lifting pour IntMap:	letouzey	2006-04-25
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	Unification max_case et max_case2	herbelin	2006-02-12
*	Unification min_case et min_case2	herbelin	2006-02-12
*	Application du souhait de transparence de well_founded_ltof (#1007)	herbelin	2005-12-30
*	legere simplification des preuves de le_S_n et pred_le	letouzey	2005-02-03
*	compatibility with POWERPC	gregoire	2004-11-22
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Typo	herbelin	2004-08-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Nouveaux thms de non circularité de nat	herbelin	2004-06-02
*	ide: silent behavior better, save icon, -byte works	marche	2004-03-03
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Nouveaux lemmes 'canoniques'; compatibilite	herbelin	2003-11-14
*	Cosmetique	herbelin	2003-11-12
*	Noms canoniques pour les variables liees	herbelin	2003-11-12
*	Independance vis a vis noms variables liees; partie sur bool dans Zbool	herbelin	2003-11-12
*	Redondances	herbelin	2003-11-05
*	Bug du commit precedent	herbelin	2003-10-27
*	Documentation/Structuration	herbelin	2003-10-22
*	Cacher les .v8	herbelin	2003-10-03
*	une induction de moins dans lt_eq_lt_dec	letouzey	2003-09-28
*	Destruct/Induction -> NewDestruct/NewInduction	herbelin	2003-09-24
*	Deplacement de le_minus de fast_integer vers Minus	herbelin	2003-06-14
*	Deplacement d'un lemme sur nat de ZArith vers Arith	herbelin	2003-06-13
*	Amelioration affichage	herbelin	2003-05-14
*	Deplacement lemmes sur fact de Reals vers Arith	herbelin	2003-05-14
*	Nouveaux lemmes	herbelin	2003-05-13
*	Nouveaux lemmes (sur proposition de Nijmegen)	herbelin	2003-05-13
*	Nouveaux lemmes (sur proposition de Nijmegen)	herbelin	2003-05-13
*	ajout inverse relation bien fondee	mohring	2003-05-09
*	Implicit Types	herbelin	2003-04-29
*	Cosmetique	herbelin	2003-04-14
*	Open Scope remplace Import	herbelin	2003-04-10
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09
*	Ajout double_plus	herbelin	2003-03-31
*	Implicit Variables Type	herbelin	2003-03-29