coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Parsing	herbelin	2001-08-10
*	Facilites pour le debogguage des univers.	coq	2001-05-29
*	nettoyage d'entrees de grammaires inutiles	courant	2001-04-09
*	branchement extraction en standard (pas de Require)	filliatr	2001-04-09
*	bug Print Proof; usage coqtop/coqc	filliatr	2001-04-06
*	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr	2001-04-04
*	Adding A command for comments, this makes it possible to have structured	bertot	2001-04-04
*	entetes	filliatr	2001-03-15
*	Ajout d'une commande pour afficher chaque coercion à la demande	herbelin	2001-02-06
*	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye	2001-02-05
*	Ajout option Set/Unset/Test Printing Coercions	herbelin	2001-01-31
*	Factorisation du '.' final	herbelin	2001-01-27
*	Token n'est plus un keyword	herbelin	2000-12-25
*	Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite	herbelin	2000-12-16
*	Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...	herbelin	2000-12-15
*	Now AddRecPath and AddPath can be used with an As option to specify the	sacerdot	2000-11-29
*	Restruration autour de qualidarg	herbelin	2000-11-26