coq - The formal proof system

Age	Commit message (Expand)	Author
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
2001-10-30	Reorganisation de Goption. Passage des options l'utilisant en synchrone	letouzey
2001-10-11	Suppression option immediate_discharge; nettoyage de Declare et conséquences	herbelin
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-10-03	Bug d'affichage du prédicat, bug d'affichage des clauses en présence de dé...	herbelin
2001-09-21	Réparation des options Set Printing and co	herbelin
2001-09-04	erreur de pretty-print lors de l'affichage de termes avec de Bruijn non lies	barras
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin
2001-05-29	Facilites pour le debogguage des univers.	coq
2001-05-03	Changement de la structure des points fixes	barras