coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Oubli d'un Set Implicit Arguments	herbelin	2003-11-07
*	Des oublis	herbelin	2003-11-06
*	Report des definitions sorties de fast_integer pour compatibilite	herbelin	2003-11-06
*	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...	herbelin	2003-11-05
*	Exporting ^; utilisation arg scope implicite	herbelin	2003-11-03
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01
*	Retour en arriere sur d'autres renommages de variables	herbelin	2003-10-28
*	Retour a un nommage non standard des variables pour compatibilite; report 're...	herbelin	2003-10-27
*	Documentation/Structuration	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Redondance de dec_eq_nat	herbelin	2003-10-21
*	Type relation dans Datatypes	herbelin	2003-10-21
*	Suppression des surcharge de regles de grammaire en v7	herbelin	2003-10-16
*	Notations pour l'exponentiation	herbelin	2003-10-13
*	Plus d'Eval Compute	herbelin	2003-10-10
*	Cacher les .v8	herbelin	2003-10-03
*	Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...	herbelin	2003-10-01
*	'_ = _ = _' maintenant predefini, meme en V7	herbelin	2003-09-30
*	'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...	herbelin	2003-09-26
*	Structuration de fast_integer en operations sur positive, proprietes des oper...	herbelin	2003-09-26
*	add_x_x de fast_integer vers auxiliary	herbelin	2003-09-25
*	Retour provisoire a une section	herbelin	2003-09-25
*	Suppression section, ce qui evite de repliquer les declarations d'Infix	herbelin	2003-09-24
*	Destruct -> NewDestruct	herbelin	2003-09-24
*	Deplacement de lemmes de IntMap vers ZArith	herbelin	2003-09-22
*	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
*	Section et report Infix hors section	herbelin	2003-09-19
*	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...	herbelin	2003-09-19
*	Bind et Delimit pour positive et Z (hors section)	herbelin	2003-09-12
*	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
*	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
*	Arguments superflus pour Zlength_nil	herbelin	2003-06-18
*	Deplacement de le_minus de fast_integer vers Minus	herbelin	2003-06-14
*	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
*	Import nat_scope	herbelin	2003-06-10
*	niveau 49 devient next	herbelin	2003-05-29
*	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin	2003-05-21
*	coqide: toolbar/autosave	monate	2003-05-07
*	Ajout Open Scope	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09