coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...	herbelin	2005-12-30
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
*	Changement des named_context	gregoire	2005-12-02
*	Affinements suite à extension Tactic Notation aux tacticielles	herbelin	2005-05-17
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Globalisation des Tactic Notation	herbelin	2005-05-15
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-25
*	Correction bug Notation: il faut re-déclarer les règles de parsing des nota...	herbelin	2004-11-22
*	Nouvelle en-tête	herbelin	2004-07-16
*	Mise en place de motifs récursifs dans Notation; quelques simplifications au...	herbelin	2004-03-17
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'	herbelin	2004-03-03
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Localisation des erreurs d'internalisation des notations de tactiques	herbelin	2004-02-12
*	reparation de qqs bugs du traducteur	barras	2004-01-26
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
*	Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...	herbelin	2003-11-20
*	Protection contre l'effacement des niveaux vides de operconstr et pattern par...	herbelin	2003-11-19
*	Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar	herbelin	2003-11-15
*	En v8, une notation, c'est 2 regles et un niveau	herbelin	2003-11-04
*	Extensibilite de la grammaires des patterns	herbelin	2003-11-01
*	On n'autorise plus les niveaux doubles L/R en v8	herbelin	2003-10-17
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Passage des projections au niveau 1	herbelin	2003-09-10
*	9 est associatif a gauche	herbelin	2003-09-10
*	Ajout construction If primitive dans constr_expr et rawconstr	herbelin	2003-09-09
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-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
*	Localisation erreurs TacAlias; Globalisation moins tolérante dans les	herbelin	2003-04-28
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	* empty log message *	barras	2003-03-12
*	Prise en compte notations dans les extensions de motiff	herbelin	2002-12-28
*	Meilleure factorisation des entrées NEXT internes	herbelin	2002-12-15
*	bug de non-indépendance des règles d'affichage et parsing vis à vis du nom...	herbelin	2002-12-03
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-12-02
*	On force l'associativité pour les entrées sans niveaux	herbelin	2002-12-02
*	Synchro level (suite)	herbelin	2002-12-01
*	Utilisation de Snext pour gérer les symboles non associatifs	herbelin	2002-11-29
*	Synchro de la table des niveaux avec les sections	herbelin	2002-11-29
*	Affinement de la gestion des niveaux toujours; type ETBigint	herbelin	2002-11-28
*	Affinement encore	herbelin	2002-11-28
*	Affinement de la gestion des niveaux	herbelin	2002-11-28
*	Correction sur commit précédent	herbelin	2002-11-27
*	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin	2002-11-26
*	MAJ delimiters et niveaux d'associativite	herbelin	2002-11-25
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24