coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-21	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-19	'::' 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-12	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-11	Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...	herbelin
2003-09-05	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-01	Passage de 'relation' à Type	herbelin
2003-08-10	Affichage {}+{}, niveau paire au plus haut	herbelin
2003-08-10	Un peu d'aide pour le traducteur	herbelin
2003-07-18	Coq.Init.Logic.eq au lieu de eq	filliatr
2003-07-08	recursion bien fondee sur des pairs	filliatr
2003-06-24	suppression de FSets (redevient une contrib)	filliatr
2003-06-24	doc	filliatr
2003-06-24	concat; debut split	filliatr
2003-06-23	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-20	remov	filliatr
2003-06-20	merge	filliatr
2003-06-20	remove_min, remove_max	filliatr
2003-06-19	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-18	AVL: suite	filliatr
2003-06-18	Arguments superflus pour Zlength_nil	herbelin
2003-06-17	AVL: suite	filliatr
2003-06-17	AVL de caml: un debut	filliatr
2003-06-16	Ground depth	filliatr
2003-06-16	reparation fsets suite a changement de Ground	filliatr
2003-06-14	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-13	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