coq - The formal proof system

Age	Commit message (Expand)	Author
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
2002-10-29	Mais laisser la syntaxe (!id) aussi disponible !	herbelin
2002-10-29	Parenthèse non obligatoires autour de !id sans argument	herbelin
2002-10-28	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin
2002-10-13	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-05-27	Ajout de Eval, Inst et Check	delahaye
2001-11-08	Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]b	herbelin
2001-08-10	Parsing	herbelin