coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout de la tactique 'remember'	herbelin	2006-10-24
*	Noms "canoniques" pour certaines des propriétés de xor.	herbelin	2006-10-17
*	Mise en forme des theories	notin	2006-10-17
*	Ajout du théorème mult_minus_distr_l	notin	2006-10-13
*	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-10-05
*	args implicites dans Field	barras	2006-09-29
*	separation de RealField	barras	2006-09-28
*	commit de field + renommages	barras	2006-09-26
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin	2006-09-22
*	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-21
*	Indentation + typo	notin	2006-09-01
*	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
*	comparison functions should be Defined not Qed	letouzey	2006-08-14
*	Renommage sqtr_lem_1 (bug 1189)	notin	2006-07-17
*	Ajout de quelques Arguments Scope pour simuler la récursivité du scope Rfun...	herbelin	2006-07-11
*	Argument Scope de list déplacé dans List.v	herbelin	2006-07-09
*	Typo	herbelin	2006-07-06
*	Quelques Hint inutiles	herbelin	2006-07-06
*	MAJ du manuel de référence	notin	2006-07-04
*	Ajout de Zgcd_spec (compat.)	notin	2006-06-26
*	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey	2006-06-25
*	repetition d'hypotheses dans well_founded_induction_type_2	letouzey	2006-06-25
*	Passage des graphes de Function dans Type	jforest	2006-06-23
*	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-09
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
*	Require FSets ne doit pas charger FSetToFiniteSet (qui utilise l'axiome d'ext...	letouzey	2006-06-05
*	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-06-04
*	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-31
*	* suite de la revision des wrappers Make	letouzey	2006-05-30
*	Ajout d'alias pour prodT_rect et cie qui avaient Ã©tÃ© oublkÃiÃ©s	herbelin	2006-05-29
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Suite changement précédence by de assert	herbelin	2006-05-24
*	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin	2006-05-23
*	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-22
*	auto with zarith genere des sous-lemmes silencieusement,	letouzey	2006-05-20