coq - The formal proof system

Age	Commit message (Expand)	Author
2003-09-21	Changement de la politique de V8only: V8only tout seul signifie	herbelin
2003-09-19	Mise en place des V8Notation et V8Infix pour déclarer des notations en	herbelin
2003-09-12	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-10	Traduction de Distfix	herbelin
2003-05-22	Ajout V8Notation	herbelin
2003-04-29	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-17	Ajout "at next level" dans Notation	herbelin
2003-04-11	Ajout option 'Local' à Infix et Notation	herbelin
2003-04-08	Ajout option "Local" à "Open Scope"	herbelin
2003-03-21	* empty log message *	barras
2003-03-12	* empty log message *	barras
2003-01-06	SearchAbout	filliatr
2002-12-15	Meilleure factorisation des entrées NEXT internes	herbelin
2002-11-29	Raffinement syntaxe Infix	herbelin
2002-11-28	Oubli	herbelin
2002-11-27	Correction sur commit précédent	herbelin
2002-11-25	MAJ delimiters et niveaux d'associativite	herbelin
2002-11-25	Retour sur le choix des delimiteurs	herbelin
2002-11-24	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-07	fix forbidden currified constructors	ddr
2002-10-22	Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...	herbelin
2002-10-21	Prise en compte des délimiteurs dans les motifs de Cases	herbelin
2002-10-14	Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une	herbelin
2002-10-13	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin
2002-08-19	Pretty-printing preliminaire des modules, commandes	coq
2002-07-15	Pour assurer une compatibilite avec la 7.3	herbelin
2002-05-30	Finalement un seul constr pour l'instant dans ExtraRedExpr	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-09-21	Réparation des options Set Printing and co	herbelin
2001-09-20	Rajout 'Set Printing Depth'	herbelin
2001-09-20	Transparent	barras
2001-08-10	Parsing	herbelin
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-04-09	nettoyage d'entrees de grammaires inutiles	courant
2001-04-09	branchement extraction en standard (pas de Require)	filliatr
2001-04-06	bug Print Proof; usage coqtop/coqc	filliatr
2001-04-04	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-03-15	entetes	filliatr
2001-02-06	Ajout d'une commande pour afficher chaque coercion à la demande	herbelin
2001-02-05	Correction pour Time pour ne pas etre oblige de mettre deux points	delahaye
2001-01-31	Ajout option Set/Unset/Test Printing Coercions	herbelin
2001-01-27	Factorisation du '.' final	herbelin
2000-12-25	Token n'est plus un keyword	herbelin
2000-12-16	Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite	herbelin
2000-12-15	Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées 'Set...	herbelin