coq - The formal proof system

Age	Commit message (Expand)	Author
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-02	Types inductifs parametriques	mohring
2005-09-06	Un vieux bug d'affichage des lieurs (cf bug #1005)	herbelin
2005-08-19	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey
2005-01-03	HUGE COMMIT	sacerdot
2004-11-16	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot
2004-09-15	hiding the meta_map in evar_defs	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-07-11	Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ...	herbelin
2004-06-28	Double bug d'affichage des cases dépendants (bug #784)	herbelin
2004-06-27	Correction affichage v8 des records avec let (bug #798)	herbelin
2004-03-28	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin
2004-03-24	bug de PP des fix (coqbugs #574)	barras
2004-03-09	bug affichage des cofix	barras
2004-03-08	correction de bugs des points fixes	barras
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-02-26	Inclusion des annotations de type des filtrages dans 'Set Printing All'	herbelin
2004-02-03	Relachement condition pour declarer un inductif dans la table des 'If'; contr...	herbelin
2004-01-29	Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit...	herbelin
2003-12-19	Substitution dans REvar; reparation bug 277	herbelin
2003-09-23	Changement de l'afficheur pour que les variables liées aient un nom indépen...	herbelin
2003-09-12	open superflu	herbelin
2003-09-09	Ajout construction If primitive dans constr_expr et rawconstr	herbelin
2003-09-06	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin
2003-08-12	Bug détypage du fix	herbelin
2003-08-11	Nouvelle mouture du traducteur v7->v8	herbelin
2003-06-10	Factorisation de detype_case pour utilisation par l'afficheur de pattern	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-04-27	Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...	herbelin
2003-03-29	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin
2003-03-12	* empty log message *	barras
2003-02-02	Bug affichage let destructurant	herbelin
2003-01-15	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin
2002-12-21	Affinement affichage	herbelin
2002-12-19	apres correction du probleme de Global.env, retour du mis_constr_nargs_env	letouzey
2002-12-17	ma bidouille marche pas...	letouzey
2002-12-13	correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...	letouzey
2002-12-09	Problèmes et améliorations divers affichage	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-05-14	Utilisation d'une construction spéciale SECVAR pour gérer la	herbelin
2002-02-14	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras
2002-02-11	substitution et pattern modulo let	barras
2002-02-07	petit nettoyage de kernel/inductive	barras
2001-12-13	compat ocaml 3.03	filliatr
2001-11-19	Bug nommage des fonctions définies par récursion mutuelle	herbelin
2001-11-19	Re-installation de l'affichage des globaux par des noms courts	herbelin
2001-11-05	GROS COMMIT:	barras