coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...	herbelin	2004-01-29
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Ajout Print Implicit avec depliage du type	herbelin	2003-11-15
*	Suppression SearchNamed finalement redondant avec SearchAbout	herbelin	2003-11-10
*	Heritage des notations v7 seulement si zero information v8	herbelin	2003-11-01
*	Ajout de Print Visibility	herbelin	2003-10-28
*	Independance de grammar.cmo vis a vis de Search	herbelin	2003-10-23
*	Integration de SearchNamed dans SearchAbout	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin	2003-10-13
*	Implantation de l'option 'format' des Notations	herbelin	2003-10-01
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	Ajout 'About'	herbelin	2003-09-26
*	Re-possibilite changement chaine infixe en passant v7 a v8	herbelin	2003-09-26
*	Distfix aussi adopte le nouveau schema de V8only	herbelin	2003-09-22
*	Changement de la politique de V8only: V8only tout seul signifie	herbelin	2003-09-21
*	Mise en place des V8Notation et V8Infix pour déclarer des notations en	herbelin	2003-09-19
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin	2003-09-12
*	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin	2003-09-12
*	Traduction de Distfix	herbelin	2003-09-10
*	Ajout V8Notation	herbelin	2003-05-22
*	Prise en compte des syntaxes v8 dans Uninterpreted Notation	herbelin	2003-04-29
*	Factorisation des produits de même type; parenthèses autour des x:=c et n:=...	herbelin	2003-04-29
*	Ajout "at next level" dans Notation	herbelin	2003-04-17
*	Ajout option 'Local' à Infix et Notation	herbelin	2003-04-11
*	Ajout option "Local" à "Open Scope"	herbelin	2003-04-08
*	* empty log message *	barras	2003-03-21
*	* empty log message *	barras	2003-03-12
*	SearchAbout	filliatr	2003-01-06
*	Meilleure factorisation des entrées NEXT internes	herbelin	2002-12-15
*	Raffinement syntaxe Infix	herbelin	2002-11-29
*	Oubli	herbelin	2002-11-28
*	Correction sur commit précédent	herbelin	2002-11-27
*	MAJ delimiters et niveaux d'associativite	herbelin	2002-11-25
*	Retour sur le choix des delimiteurs	herbelin	2002-11-25
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	fix forbidden currified constructors	ddr	2002-11-07
*	Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...	herbelin	2002-10-22
*	Prise en compte des délimiteurs dans les motifs de Cases	herbelin	2002-10-21
*	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin	2002-10-14
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin	2002-10-13
*	Pretty-printing preliminaire des modules, commandes	coq	2002-08-19
*	Pour assurer une compatibilite avec la 7.3	herbelin	2002-07-15
*	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin	2002-05-30
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin	2001-10-11
*	Réparation des options Set Printing and co	herbelin	2001-09-21
*	Rajout 'Set Printing Depth'	herbelin	2001-09-20
*	Transparent	barras	2001-09-20