coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Conflit de nom Pplus dans positive et dans polynomial (de ring)	herbelin	2003-09-21
*	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin	2003-09-21
*	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin	2003-09-21
*	Nettoyage	herbelin	2003-09-21
*	'::' est deja pris en V7	herbelin	2003-09-19
*	Section et report Infix hors section	herbelin	2003-09-19
*	Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...	herbelin	2003-09-19
*	Ajout notation :: pour cons	herbelin	2003-09-19
*	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...	herbelin	2003-09-19
*	Suppression DatatypesSyntax et PeanoSyntax qui était vides	herbelin	2003-09-12
*	Ajout et MAJ commandes de scopes	herbelin	2003-09-12
*	Bind et Delimit pour R	herbelin	2003-09-12
*	Bind et Delimit pour nat	herbelin	2003-09-12
*	Bind et Delimit pour positive et Z (hors section)	herbelin	2003-09-12
*	Bind et Delimit pour R	herbelin	2003-09-12
*	Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...	herbelin	2003-09-11
*	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