coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ordre (symbolique) des Require	herbelin	2003-10-28
*	Passage de la notations de paire dans core_scope	herbelin	2003-10-28
*	Passage des notations de type dans type_scope	herbelin	2003-10-28
*	Ajout %core; MAJ niveau connecteurs logique	herbelin	2003-10-28
*	Commentaires	herbelin	2003-10-23
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Maintenant avant Datatypes	herbelin	2003-10-21
*	ajouts	herbelin	2003-10-21
*	Des implicites plus 'naturels' pour eq_ind, identity_ind and co	herbelin	2003-10-17
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	Argument de except, error implicite seulement en v8; Changement 'as notation'...	herbelin	2003-10-14
*	Argument de None implicite seulement en v8	herbelin	2003-10-14
*	Argument implicite pour None, error, except	herbelin	2003-10-13
*	Enregistrement '^' en v8	herbelin	2003-10-13
*	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
*	Delimiters N devient 'nat'	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Cacher les .v8	herbelin	2003-10-03
*	well_founded_induction de nouveau transparent	letouzey	2003-09-28
*	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
*	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
*	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
*	Bind et Delimit pour nat	herbelin	2003-09-12
*	Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...	herbelin	2003-09-11
*	Affichage {}+{}, niveau paire au plus haut	herbelin	2003-08-10
*	recursion bien fondee sur des pairs	filliatr	2003-07-08
*	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
*	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
*	V8Notation	herbelin	2003-05-22
*	Ajout V8Notation	herbelin	2003-05-22
*	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin	2003-05-21
*	Blancs	herbelin	2003-04-29
*	Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot	letouzey	2003-04-28
*	Intégration DatatypesSyntax à Datatypes	herbelin	2003-04-17
*	Intégration DatatypesSyntax à Datatypes	herbelin	2003-04-17
*	Syntaxe 'x=y:>T'	herbelin	2003-04-17
*	Activation des implicites pour la v8	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09