coq - the Coq proof assistant

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