coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Suppression des alias eqT/exT/exT2 en nouvelle syntaxe	herbelin	2003-03-31
*	Notation eqT superflue	herbelin	2003-03-31
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	Déplacement de minus dans Peano	herbelin	2003-03-29
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
*	* empty log message *	barras	2003-03-21
*	* empty log message *	barras	2003-03-14
*	* empty log message *	barras	2003-03-12
*	Pb de parenthèse dans "Check (S (plus O O))"	herbelin	2003-01-30
*	Une entrée spéciale "annot" pour les piquants	herbelin	2002-12-15
*	Ajout syntaxe '>'	herbelin	2002-12-15
*	Essai d'introduction d'un scope des types	herbelin	2002-12-03
*	Re-échappement des \ et " dans les token string	herbelin	2002-11-29
*	Simplification	herbelin	2002-11-28
*	Essai de suppression du caractere d'echappement des string	herbelin	2002-11-28
*	Plus de précisions	herbelin	2002-11-28
*	Retour sur associativité à droite de * pour compatibilité de prod	herbelin	2002-11-27
*	Ne pas cacher les Metas d'une notations, ils peuvent être liant dans	herbelin	2002-11-26
*	Plus d'indication pour le gestionnaire de niveaux	herbelin	2002-11-26
*	Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiques	herbelin	2002-11-26
*	Bug niveau	herbelin	2002-11-26
*	Retablissement SynDef Value/Error	herbelin	2002-11-25
*	Oubli	herbelin	2002-11-25
*	Généralisation de l'utilisation de Notation	herbelin	2002-11-24