coq - The formal proof system

Age	Commit message (Expand)	Author
2003-01-16	Bugs affichage	herbelin
2003-01-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2003-01-15	Nouvelle interprétation des nombres réels	desmettr
2003-01-09	Export M + Module M <: SIG	coq
2003-01-07	Retour printer ast pour V7.4	herbelin
2003-01-06	SearchAbout	filliatr
2002-12-28	Prise en compte notations dans les extensions de motiff	herbelin
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-21	Affinement affichage	herbelin
2002-12-21	Plus de notation cablees dans 'annot'	herbelin
2002-12-19	Petit netoyage dans lib	coq
2002-12-19	bug: Global.env() executé au chargement -> eta-expansion	letouzey
2002-12-15	Meilleure factorisation des entrées NEXT internes	herbelin
2002-12-15	Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxe	herbelin
2002-12-15	Pas de 0 dans positive	herbelin
2002-12-13	possibilité de faire Print M avec M module ou modtype au lieu de Print Modul...	letouzey
2002-12-12	Ajout du vernac Proof with	gregoire
2002-12-10	Bugs divers	herbelin
2002-12-10	Ajout options -v7 et -v8, et commandes V7only et V8only	herbelin
2002-12-09	Problèmes et améliorations affichage; Changement Simpl	herbelin
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-12-04	Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...	herbelin
2002-12-04	Modification Require From	mohring
2002-12-03	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey
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	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-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	Re-déplacement du résultat de Grammar au niveau constr_expr	herbelin
2002-12-02	On force l'associativité pour les entrées sans niveaux	herbelin
2002-12-01	Synchro level (suite)	herbelin
2002-11-29	Raffinement syntaxe Infix	herbelin
2002-11-29	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	constr9 et lconstr NONA pour une meilleur extensibilité	herbelin
2002-11-29	Re-échappement des \ et " dans les token string	herbelin
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	Essai de suppression du caractere d'echappement des string	herbelin
2002-11-28	Oubli	herbelin
2002-11-28	Affinement encore	herbelin
2002-11-28	Affinement de la gestion des niveaux	herbelin
2002-11-27	Correction sur commit précédent	herbelin
2002-11-26	Oubli	herbelin
2002-11-26	Réaffichage des Syntactic Definition (printer constr_expr).	herbelin
2002-11-25	Retablissement Syntactic Definition	herbelin