coq - The formal proof system

Age	Commit message (Expand)	Author
2007-01-12	Suite au mail de Lionel a propos du Makefile:	letouzey
2004-07-16	Nouvelle en-tête	herbelin
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2002-12-09	chamboulement du codage des indcutifs extraits; deplacements des tables; ...	letouzey
2002-11-18	remaniement de test_extraction.v	letouzey
2002-10-31	L'extraction c'est magic cvs -n up	letouzey
2002-07-16	maj	letouzey
2002-07-16	Gros Remaniement Extraction:	letouzey
2002-03-28	reparation du cas des arguments de type qui sont des arités + patch dummy ap...	letouzey
2002-03-26	Refonte complete de la génération des types ML	letouzey
2002-03-21	considerations de pretty-print	letouzey
2002-03-15	gros commit: principalement ajout des lambdas arity + leur optimisation en te...	letouzey
2002-03-05	cas des constructeurs singletons. Messages d'erreur. Revision de test_extract...	letouzey
2001-09-20	correction du eta_expanse	letouzey
2001-05-22	suite du musée des horreurs	letouzey
2001-05-11	bug cast	letouzey
2001-05-10	exemples Magic	letouzey
2001-04-10	bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_app	letouzey
2001-03-28	changement type_var et signature	filliatr
2001-03-27	conservation des arguments dans Prop (snif)	filliatr
2001-03-27	trace des inductifs sur Prop	letouzey
2001-03-23	eta-expansion des constructeurs si necessaire (a posteriori en miniML)	filliatr
2001-03-23	suppression des param dans inductifs. suite du Cases	letouzey
2001-03-21	Reecriture du extract_type pour Prod et Lambda. Eta-expansion dans les branch...	letouzey
2001-03-20	extraction naive de fix et case	filliatr
2001-03-20	Extract_term_with_type. mise a jour & verification des commentaires	letouzey
2001-03-15	entetes	filliatr
2001-03-14	interface du extract_rec. Extract_constr prend un environnement	letouzey
2001-03-13	signatures dans le bon ordre	filliatr
2001-03-13	Finite	filliatr
2001-03-13	simplification: plus de contexte pour extract_type et contexte simplifié pou...	filliatr
2001-03-13	suite de la verification des assert false	letouzey
2001-03-12	mise a jour commentaires'	filliatr
2001-03-12	Commentaires. Verification des assert false. Probleme des types ML arity.	letouzey
2001-03-07	distinction contexte et signature	filliatr