coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-13	Ajout du théorème mult_minus_distr_l	notin
2006-10-05	revert, the previous commit was a mistake	bertot
2006-10-05	A version of natprering that should be more efficient and removal of a bad	bertot
2006-10-05	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey
2006-10-05	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras
2006-09-29	args implicites dans Field	barras
2006-09-28	separation de RealField	barras
2006-09-26	commit de field + renommages	barras
2006-09-26	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras
2006-09-22	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin
2006-09-21	incomplete and temporary fix for PR#1222: revert accepts up to 10 args	letouzey
2006-09-21	better scope/require managment (patch by Russel O'Connor)	letouzey
2006-09-01	Indentation + typo	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-08-14	comparison functions should be Defined not Qed	letouzey
2006-07-17	Renommage sqtr_lem_1 (bug 1189)	notin
2006-07-11	Ajout de quelques Arguments Scope pour simuler la récursivité du scope Rfun...	herbelin
2006-07-09	Argument Scope de list déplacé dans List.v	herbelin
2006-07-06	Typo	herbelin
2006-07-06	Quelques Hint inutiles	herbelin
2006-07-04	MAJ du manuel de référence	notin
2006-06-26	Ajout de Zgcd_spec (compat.)	notin
2006-06-25	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey
2006-06-25	repetition d'hypotheses dans well_founded_induction_type_2	letouzey
2006-06-23	Passage des graphes de Function dans Type	jforest
2006-06-09	Modification déf de exists! pour éviter une éta-expansion et pouvoir être...	herbelin
2006-06-09	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...	herbelin
2006-06-06	+ ameliorating the tactic "functional induction"	jforest
2006-06-05	Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext...	letouzey
2006-06-04	Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin
2006-05-31	ajout de QArith dans les theories standards	letouzey
2006-05-31	petits ajouts	letouzey
2006-05-31	Replacing the old version of "functional induction" with the new one.	jforest
2006-05-30	* suite de la revision des wrappers Make	letouzey
2006-05-29	Ajout d'alias pour prodT_rect et cie qui avaient Ã©tÃ© oublkÃiÃ©s	herbelin
2006-05-28	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin
2006-05-24	Suite changement précédence by de assert	herbelin
2006-05-23	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin
2006-05-22	un debut de propriétés concernant FMap	letouzey
2006-05-22	suite des marquages de types et opacifications de lemmes dans les wrappers Make	letouzey
2006-05-22	MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...	herbelin
2006-05-22	MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ba...	herbelin
2006-05-20	auto with zarith genere des sous-lemmes silencieusement,	letouzey
2006-05-20	suite tentative pour permettre l'utilisation de modules de FSets	letouzey
2006-05-19	on cache autant que possible Raw dans FSet(Weak)List.Make	letouzey
2006-05-18	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...	letouzey