coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	suite tentative pour permettre l'utilisation de modules de FSets	letouzey	2006-05-20
*	on cache autant que possible Raw dans FSet(Weak)List.Make	letouzey	2006-05-19
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8829 85f007b7-540e-04...	letouzey	2006-05-18
*	Typo dans List.v	notin	2006-05-17
*	Ajout de [count_occ] dans List.v	notin	2006-05-17
*	etoffage des notions de permutations (a la fois List.Permutation et Permutati...	letouzey	2006-05-16
*	3*rien	letouzey	2006-05-15
*	ajout d'exemples de decidable types	letouzey	2006-05-15
*	petit ajout concernant InA	letouzey	2006-05-15
*	On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos	letouzey	2006-05-14
*	In_dec de nouveau transparent	letouzey	2006-05-14
*	reparartion d'un petit oubli cassant PrecedenceGraph	letouzey	2006-05-14
*	typo	letouzey	2006-05-13
*	un Zgcd calculant dans coq	letouzey	2006-05-13
*	une fonction pouvant calculer le gcd en coq	letouzey	2006-05-11