coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	mise a jour nouvelle syntaxe	barras	2003-10-11
*	nat_scope ouvert par defaut	herbelin	2003-10-10
*	identity est equivalent sur Type (sauf sans argument)	herbelin	2003-10-10
*	type_scope	herbelin	2003-10-10
*	Suppression de definitions equivalentes	herbelin	2003-10-10
*	Notation '^'	herbelin	2003-10-10
*	Plus d'Eval Compute	herbelin	2003-10-10
*	MAJ commentaires	herbelin	2003-10-10
*	Delimiters N devient 'nat'	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Renommage en v8 de PolyList en List et List en MonoList	herbelin	2003-10-10
*	Renommage en v8 de PolyList en List et List en MonoList	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
*	une induction de moins dans lt_eq_lt_dec	letouzey	2003-09-28
*	well_founded_induction de nouveau transparent	letouzey	2003-09-28
*	'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...	herbelin	2003-09-26
*	Induction -> NewInduction; '++' pour app	herbelin	2003-09-26
*	Passage de Destruct a NewDestruct; '-' pour negb	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/Induction -> NewDestruct/NewInduction	herbelin	2003-09-24
*	Destruct -> NewDestruct	herbelin	2003-09-24
*	Remplacement de Induction/Destruct par NewInduction/NewDestruct	herbelin	2003-09-23
*	Remplacement de Induction/Destruct par NewInduction/NewDestruct	herbelin	2003-09-23
*	Remplacement de Induction/Destruct par NewInduction/NewDestruct	herbelin	2003-09-23
*	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin	2003-09-23
*	traducteur: affiche les commentaires a l'interieur des commandes	barras	2003-09-22
*	Implicits maintenant au courant pour l'affichage	herbelin	2003-09-22
*	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
*	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