coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add f_equal case for 6 arguments.	msozeau	2007-01-02
*	Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à	herbelin	2006-12-28
*	Remplacement de la définition de Pind et Prec par une définition	herbelin	2006-12-28
*	Changement dans ring et field, beaucoup de correction d'erreurs,	bgregoir	2006-12-15
*	Dépendence inutile	herbelin	2006-12-12
*	AllÃègement de syntxe suite à l'introduction de l'unif pattern	herbelin	2006-12-12
*	Bug nommage Zgt_trans_succ	herbelin	2006-12-12
*	correction Open Local Scope (Ring)	bgregoir	2006-12-11
*	Changement dans le kernel :	bgregoir	2006-12-11
*	fixes PR#1269 about function: there is no reason well founded induction is	bertot	2006-11-05
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	LegacyRfield was opening R_scope	barras	2006-10-30
*	simplif de la partie ML de ring/field	barras	2006-10-27
*	Le caractère ² fait planter make doc	notin	2006-10-27
*	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin	2006-10-26
*	oups, ne chargeait pas les bons fichiers	letouzey	2006-10-25
*	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