coq - The formal proof system

Age	Commit message (Expand)	Author
2008-07-20	Extraction: better dependency computation (after optimisations)	letouzey
2008-05-07	export Extract_env.mono_environment in the mli	letouzey
2008-04-16	first-order --> firstorder (kills a warning about not being a valid id)	letouzey
2008-04-15	fix some bogus calls to id_of_string by the extraction	letouzey
2008-03-14	nettoyage de code obsolete.	soubiran
2008-03-14	Ajout des alias de module dans le noyau.	soubiran
2008-03-05	Attempt of fix for extraction of modules types	letouzey
2008-02-27	dead code	letouzey
2008-02-27	typo	letouzey
2008-02-01	Beaoucoup de changements dans la representation interne des modules.	soubiran
2008-01-22	Récupération d'une exception Not_found	notin
2008-01-20	cosmetics: after an extract inductive to bool, let's use if then else	letouzey
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-11-21	Extraction inlines Wf.Fix by default (wish of Y.Bertot)	letouzey
2007-10-25	small fix of commit 10188: a string given via Extract Inductive can be empty	letouzey
2007-10-21	An error message instead of an empty extraction when the monolithic	letouzey
2007-10-21	Avoid the auto-inlining of small fixpoints like List.map.	letouzey
2007-10-17	Repair Haskell/Scheme extraction in the new extraction backend design:	letouzey
2007-10-17	Major reorganisation of the extraction "backend".	letouzey
2007-10-09	Extraction now checks that the required libraries are indeed loaded (bug #1144)	letouzey
2007-10-09	forbid extraction under a module type	letouzey
2007-10-09	Extract Inline/Inductive/Constant can now be used from inside a module	letouzey
2007-10-08	Better use of tables for storing results of extract_ind (bug #1709)	letouzey
2007-10-06	Allowing infix constructors/types in a Extract Inductive	letouzey
2007-10-06	Extraction: factorisation of identical branches in a match	letouzey
2007-07-12	Deletion of contrib/extraction/test	letouzey
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-01-12	Suite au mail de Lionel a propos du Makefile:	letouzey
2007-01-12	un saut de ligne ...	letouzey
2007-01-05	suite de la reparation du bug 1239: apres les inds, les records et vars de types	letouzey
2006-12-17	reparation bug 1239	letouzey
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-04	Correction bug #1211	notin
2006-07-07	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin
2006-06-09	oups: il faut penser a fermer la porte en partant (d'un fixpoint)	letouzey
2006-06-09	changements de dernieres minutes pour la 8.1 beta:	letouzey
2006-06-08	reparation bug 1006	letouzey
2006-06-02	debut de reparation du test d'extraction	letouzey
2006-06-01	reparation bug #1128	letouzey
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-20	decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)	letouzey
2005-12-28	Remplacement Pp.qs par Pptactic.qsnew	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-12-21	Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...	herbelin
2005-12-16	amelioration de l'extraction haskell: affichage du type des fonctions, et sup...	letouzey
2005-12-16	multiples ameliorations de l'extraction scheme:	letouzey