coq - The formal proof system

Age	Commit message (Expand)	Author
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-02-06	pushed evar reduction in kernel	barras
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-05-15	really fixed Georges\' bug	barras
2008-05-14	corrige le bug de Georges	barras
2008-05-12	Changement de stratégie vis à vis du commit 10859 sur la gestion des	herbelin
2008-04-27	Correction du bug des types singletons pas sous-type de Set	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-04-20	Add the ability to give a transparent_state for conversion, to	msozeau
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2006-05-03	bug #1096: whd_stack on one arg of conversion had side-effect on the other arg	barras
2005-12-02	Changement des named_context	gregoire
2004-11-22	compatibility with POWERPC	gregoire
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-08-05	Improved reduction machine with closure: should use less memory	barras
2003-06-30	Comparaison de Cases module mind_equiv	coq
2003-04-08	test: un boolean et une fonction check_for_interrupt inseree dans la conversi...	filliatr
2002-08-16	Strengthenning rules for modules + No modules in sections	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-07	Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)	herbelin
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin
2001-07-03	Depliage des let-in dans le test de garde	herbelin
2001-07-02	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin
2001-05-23	amelioration des messages d'erreurs vis a vis des evars	barras
2001-05-03	Changement de la structure des points fixes	barras
2001-04-23	reduction des let in dans whd_programs	filliatr
2001-04-11	réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...	filliatr
2001-04-10	réparation Correctness; options Extraction (changement de syntaxe)	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-23	amelioration de la consommation memoire de la conversion en eta-expansant	barras
2001-03-15	entetes	filliatr
2001-03-01	nouvelle implantation de la reduction	barras
2001-02-28	retire profile	mohring
2001-02-28	Changement de subst_meta	mohring
2000-12-26	Déplacement du type stack de Reduction vers Closure et utilisation pour acc�...	herbelin
2000-12-20	Bug mauvais environnement dans le test d'eta-conversion	herbelin
2000-11-27	Ajout map_constr_with_full_binders et strong pour Simpl	herbelin
2000-11-22	deplacement poly_args; iterateurs sur les segments	filliatr
2000-11-02	suppression des (* open Generic *)	filliatr
2000-10-26	Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ...	herbelin
2000-10-24	Bug réduction suite modifs let-in	herbelin