coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	principes de récurrences plus efficaces pour l'extraction	letouzey	2003-09-05
*	Zdiv plus efficace: r+r -> 2*r	letouzey	2003-09-05
*	Zabs_Zsgn	letouzey	2003-09-05
*	Passage de 'relation' à Type	herbelin	2003-09-01
*	Affichage {}+{}, niveau paire au plus haut	herbelin	2003-08-10
*	Un peu d'aide pour le traducteur	herbelin	2003-08-10
*	Coq.Init.Logic.eq au lieu de eq	filliatr	2003-07-18
*	recursion bien fondee sur des pairs	filliatr	2003-07-08
*	suppression de FSets (redevient une contrib)	filliatr	2003-06-24
*	doc	filliatr	2003-06-24
*	concat; debut split	filliatr	2003-06-24
*	join	filliatr	2003-06-23
*	add_tree : sur type tree plutot que sur type t	filliatr	2003-06-23
*	merge_bis et debug join	filliatr	2003-06-23
*	remov	filliatr	2003-06-20
*	merge	filliatr	2003-06-20
*	remove_min, remove_max	filliatr	2003-06-20
*	add	filliatr	2003-06-19
*	bal: preuve terminee	filliatr	2003-06-19
*	bal: premier cas hl > hr + 2	filliatr	2003-06-19
*	typo	filliatr	2003-06-19
*	AVL: suite	filliatr	2003-06-18
*	Arguments superflus pour Zlength_nil	herbelin	2003-06-18
*	AVL: suite	filliatr	2003-06-17
*	AVL de caml: un debut	filliatr	2003-06-17
*	Ground depth	filliatr	2003-06-16
*	reparation fsets suite a changement de Ground	filliatr	2003-06-16
*	Deplacement de le_minus de fast_integer vers Minus	herbelin	2003-06-14
*	Deplacement de le_minus de fast_integer vers Minus	herbelin	2003-06-14
*	changement de spécif du fold	letouzey	2003-06-13
*	fcts tail-recursives	filliatr	2003-06-13
*	Require Export	filliatr	2003-06-13
*	FSets, mais pas compile' par make world	filliatr	2003-06-13
*	suite changements ZArith en vu de librairie FSet	letouzey	2003-06-13
*	quelques adaptations de Zarith en vu de la nouvelle librarie FSet	letouzey	2003-06-13
*	Deplacement d'un lemme sur nat de ZArith vers Arith	herbelin	2003-06-13
*	INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...	herbelin	2003-06-12
*	Import nat_scope	herbelin	2003-06-10
*	Suppression d'une occurrence superflue d'argument de type dans Notation sacha...	herbelin	2003-06-10
*	Deplacement delimiteur T dans Notations	herbelin	2003-06-10
*	Bug niveau	herbelin	2003-05-29
*	niveau 49 devient next	herbelin	2003-05-29
*	niveau 49 devient next	herbelin	2003-05-29
*	Ne pas mettre d'associatif a droite au niveau 3 en V7	herbelin	2003-05-29
*	'only parsing' pour le passage de trucT a truc	herbelin	2003-05-27
*	"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals	herbelin	2003-05-24
*	V8Notation	herbelin	2003-05-22
*	Ajout V8Notation	herbelin	2003-05-22
*	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin	2003-05-21
*	Notations	herbelin	2003-05-21