coq - The formal proof system

Age	Commit message (Expand)	Author
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-02-16	Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.	msozeau
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-01	Abbreviation of order notation.	msozeau
2007-01-31	Fix order of wf and measure arguments, patch Program doc.	msozeau
2006-12-03	Remplacement de la dépendance de G_vernac en G_constr (source	herbelin
2006-10-09	Notations:	herbelin
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir
2006-07-12	Correction incohérence parsing de %delim dans les motifs	herbelin
2006-07-04	Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ...	herbelin
2006-07-03	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin
2006-06-22	Added {measure x f} as a valid recursion order.	msozeau
2006-05-29	The "clean integration of subtac" patch.	msozeau
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2005-12-30	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-02	Changement des named_context	gregoire
2004-12-24	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin
2004-11-17	Déclaration de '..' comme mot-clé (résoud bug #856)	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-03-17	Parsing des V8Notation avec motif recursif en v7	herbelin
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-02-26	Keep structure information for Fixpoint declaration and Fix terms	bertot
2003-11-14	Compatibilite %T	herbelin
2003-11-03	Compatibilite V7.4 pour le delimiteur de positive	herbelin
2003-10-10	Delimiters N devient 'nat'	herbelin
2003-09-22	traducteur: affiche les commentaires a l'interieur des commandes	barras
2003-09-21	Mise en place d'implicites par noms en v8	herbelin
2003-09-12	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-11	Token '.(' seulement pour v8, sinon conflit avec '.(*'	herbelin
2003-06-10	Ajout notation c.(f) en v8 pour les projections de Record	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-03-27	Affinement nommage des productions	herbelin
2003-03-12	* empty log message *	barras
2003-02-17	Affinement entree annot	herbelin
2003-01-30	Adds a possibility to construct a term as if it had been parsed through	bertot
2002-12-21	Plus de notation cablees dans 'annot'	herbelin
2002-12-15	Meilleure factorisation des entrées NEXT internes	herbelin
2002-12-02	Associativité de constr9 et lconst à RIGHTA qui est le plus courant	herbelin
2002-11-29	constr9 et lconstr NONA pour une meilleur extensibilité	herbelin
2002-11-28	Essai d'une autre syntaxe pour la dlimitation des scopes	herbelin
2002-11-26	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin
2002-11-24	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin
2002-11-15	Passage à une représentation des fixpoints plus primitive dans constr_expr ...	herbelin
2002-11-14	Bug factorisation	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-07	Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...	herbelin