coq - The formal proof system

Age	Commit message (Expand)	Author
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
2000-11-29	Now AddRecPath and AddPath can be used with an As option to specify the	sacerdot
2000-11-26	Restruration autour de qualidarg	herbelin
2000-11-24	SearchPattern et SearchRewrite	filliatr
2000-11-22	deplacement poly_args; iterateurs sur les segments	filliatr
2000-11-20	Prise en compte des noms qualifiés dans certaines commandes; nouveau lexeme ...	herbelin
2000-11-08	nouveau load path	filliatr
2000-11-03	compilation des fichiers ml4 sans GNUseries	filliatr
2000-10-18	Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...	herbelin
2000-10-17	Pb factorisation de Print Grammar	herbelin
2000-09-10	Ajout d'un LetIn primitif.	herbelin
2000-07-28	Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...	herbelin
2000-07-26	Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour Time ou Gra...	herbelin
2000-05-03	Ajout du langage de tactiques	delahaye
2000-01-20	Bête renommage	herbelin
2000-01-13	Nettoyage des fichiers de parsing	herbelin
2000-01-07	Renommage command en constr	herbelin
1999-09-08	compilation des grammaires (ouf)	filliatr
1999-09-08	modules grammaire Coq	filliatr