coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Déclaration de '..' comme mot-clé (résoud bug #856)	herbelin	2004-11-17
*	Nouvelle en-tête	herbelin	2004-07-16
*	Parsing des V8Notation avec motif recursif en v7	herbelin	2004-03-17
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	Compatibilite %T	herbelin	2003-11-14
*	Compatibilite V7.4 pour le delimiteur de positive	herbelin	2003-11-03
*	Delimiters N devient 'nat'	herbelin	2003-10-10
*	traducteur: affiche les commentaires a l'interieur des commandes	barras	2003-09-22
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
*	Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...	herbelin	2003-09-12
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Token '.(' seulement pour v8, sinon conflit avec '.(*'	herbelin	2003-06-11
*	Ajout notation c.(f) en v8 pour les projections de Record	herbelin	2003-06-10
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Affinement nommage des productions	herbelin	2003-03-27
*	* empty log message *	barras	2003-03-12
*	Affinement entree annot	herbelin	2003-02-17
*	Adds a possibility to construct a term as if it had been parsed through	bertot	2003-01-30
*	Plus de notation cablees dans 'annot'	herbelin	2002-12-21
*	Meilleure factorisation des entrées NEXT internes	herbelin	2002-12-15
*	Associativité de constr9 et lconst à RIGHTA qui est le plus courant	herbelin	2002-12-02
*	constr9 et lconstr NONA pour une meilleur extensibilité	herbelin	2002-11-29
*	Essai d'une autre syntaxe pour la dlimitation des scopes	herbelin	2002-11-28
*	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin	2002-11-26
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24
*	Passage à une représentation des fixpoints plus primitive dans constr_expr ...	herbelin	2002-11-15
*	Bug factorisation	herbelin	2002-11-14
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...	herbelin	2002-11-07
*	Mais laisser la syntaxe (!id) aussi disponible !	herbelin	2002-10-29
*	Parenthèse non obligatoires autour de !id sans argument	herbelin	2002-10-29
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-28
*	Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...	herbelin	2002-10-13
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	Ajout de Eval, Inst et Check	delahaye	2002-05-27
*	Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]b	herbelin	2001-11-08
*	Parsing	herbelin	2001-08-10
*	Extension des parametres de Clear + Inst	delahaye	2001-06-19
*	Interpretation MetaId + Progress + Inst	delahaye	2001-06-18
*	Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Case	clrenard	2001-06-11
*	Non parenthesage des applications de tactiques	delahaye	2001-04-14
*	entetes	filliatr	2001-03-15
*	Acceptation des noms qualifiés; nouveau lexeme METAIDENT pour les $id	herbelin	2000-11-20
*	compilation des fichiers ml4 sans GNUseries	filliatr	2000-11-03
*	Suppression de Abst	herbelin	2000-09-10
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
*	Pattern matching de sous-termes + exceptions dans le lexer	delahaye	2000-08-17
*	- $BINDER -> BINDER dans g_constr.ml4 (=> erreur syntax Fix)	filliatr	2000-06-21
*	Ajout du langage de tactiques	delahaye	2000-05-03