coq - The formal proof system

Age	Commit message (Expand)	Author
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	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	Bind et Delimit pour nat	herbelin
2003-09-11	Suppression notations redondantes en v8 : Fst, ProjS1, Value, Ex ...	herbelin
2003-08-10	Affichage {}+{}, niveau paire au plus haut	herbelin
2003-07-08	recursion bien fondee sur des pairs	filliatr
2003-06-10	Suppression d'une occurrence superflue d'argument de type dans Notation sacha...	herbelin
2003-06-10	Deplacement delimiteur T dans Notations	herbelin
2003-05-29	Bug niveau	herbelin
2003-05-29	Ne pas mettre d'associatif a droite au niveau 3 en V7	herbelin
2003-05-27	'only parsing' pour le passage de trucT a truc	herbelin
2003-05-22	V8Notation	herbelin
2003-05-22	Ajout V8Notation	herbelin
2003-05-21	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin
2003-04-29	Blancs	herbelin
2003-04-28	Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot	letouzey
2003-04-17	Intégration DatatypesSyntax à Datatypes	herbelin
2003-04-17	Intégration DatatypesSyntax à Datatypes	herbelin
2003-04-17	Syntaxe 'x=y:>T'	herbelin
2003-04-09	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-03-31	Suppression des alias eqT/exT/exT2 en nouvelle syntaxe	herbelin
2003-03-31	Notation eqT superflue	herbelin
2003-03-29	eq fusionne avec eqT et devient par défaut sur Type,	herbelin
2003-03-29	Déplacement de minus dans Peano	herbelin
2003-03-28	notations <>, Assumption avec existentiel, replace term	mohring
2003-03-21	* empty log message *	barras
2003-03-14	* empty log message *	barras
2003-03-12	* empty log message *	barras
2003-01-30	Pb de parenthèse dans "Check (S (plus O O))"	herbelin
2002-12-15	Une entrée spéciale "annot" pour les piquants	herbelin
2002-12-15	Ajout syntaxe '>'	herbelin
2002-12-03	Essai d'introduction d'un scope des types	herbelin
2002-11-29	Re-échappement des \ et " dans les token string	herbelin
2002-11-28	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-27	Retour sur associativité à droite de * pour compatibilité de prod	herbelin
2002-11-26	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-25	Retablissement SynDef Value/Error	herbelin
2002-11-25	Oubli	herbelin
2002-11-24	Généralisation de l'utilisation de Notation	herbelin
2002-11-20	Les parenthèses de la notation '(n)' maintemant mises par ML pour un meilleu...	herbelin
2002-11-14	Oubli	herbelin