coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Modification Require From	mohring	2002-12-04
*	Correction d'un message d'erreur de l'application de non-foncteur	coq	2002-12-04
*	mdule --> module	mohring	2002-12-04
*	suppression du champ mind_singl inutilisé dans mutual_inductive_body	letouzey	2002-12-04
*	Corrige un bug de composition de substitutions	coq	2002-12-04
*	fichiers DOS	filliatr	2002-12-04
*	maj	filliatr	2002-12-04
*	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey	2002-12-03
*	MAJ travail moulinette	herbelin	2002-12-03
*	bug de non-indépendance des règles d'affichage et parsing vis à vis du nom...	herbelin	2002-12-03
*	bugs d'affichage (confusion key/scope dans les délimiteurs)	herbelin	2002-12-03
*	Préparation à la prise en compte des changements de scopes internes aux not...	herbelin	2002-12-03
*	MAJ	herbelin	2002-12-03
*	Essai d'introduction d'un scope des types	herbelin	2002-12-03
*	Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles	bertot	2002-12-03
*	Pas de globalisation impérative pour les Grammar	herbelin	2002-12-03
*	Calcul de l'associativité même pour les Grammar avec plusieurs clauses	herbelin	2002-12-03
*	Le '.' peut faire partie d'un token	herbelin	2002-12-03
*	maj	filliatr	2002-12-03
*	Remplacement Grammar par Notation	herbelin	2002-12-02
*	MAJ sur MAJ	herbelin	2002-12-02
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-12-02
*	Associativité de constr9 et lconst à RIGHTA qui est le plus courant	herbelin	2002-12-02
*	Ajout des options "Set Contextual Implicits" et "Set Strict Implicits	herbelin	2002-12-02
*	Re-déplacement du résultat de Grammar au niveau constr_expr (globalisation ...	herbelin	2002-12-02
*	Ajout des options "Set Contextual Implicits" et "Set Strict Implicits	herbelin	2002-12-02
*	Re-déplacement du résultat de Grammar au niveau constr_expr	herbelin	2002-12-02
*	Z_scope doit annuler l'affichage de = entre	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
*	maj	filliatr	2002-11-30
*	2 bugs: 1) projections pas renommées 2) mutual fixpoints a l'envers	letouzey	2002-11-29
*	Raffinement syntaxe Infix	herbelin	2002-11-29
*	Utilisation de Snext pour gérer les symboles non associatifs	herbelin	2002-11-29
*	MAJ	herbelin	2002-11-29
*	Synchro de la table des niveaux avec les sections	herbelin	2002-11-29
*	constr9 et lconstr NONA pour une meilleur extensibilité	herbelin	2002-11-29
*	Re-échappement des \ et " dans les token string	herbelin	2002-11-29
*	maj	filliatr	2002-11-29
*	cosmetique	letouzey	2002-11-29
*	Remaniement du pp, suite: vers un renommage modulaire correcte	letouzey	2002-11-28
*	Quelques Set et Map spécialisés	letouzey	2002-11-28
*	Affinement de la gestion des niveaux toujours; type ETBigint	herbelin	2002-11-28
*	Essai d'une autre syntaxe pour la dlimitation des scopes	herbelin	2002-11-28
*	Ajout d'une entre Prim.bigint	herbelin	2002-11-28
*	Court-circuit de g_zsyntax	herbelin	2002-11-28
*	Bug exception	herbelin	2002-11-28
*	Court-circuit de g_zsyntax	herbelin	2002-11-28
*	Simplification	herbelin	2002-11-28
*	Essai de suppression du caractere d'echappement des string	herbelin	2002-11-28