coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	added isProd to term.mli.	coq	2006-02-16
*	Variable inutilisée	herbelin	2006-01-21
*	* empty log message *	barras	2006-01-20
*	Suppression résidus code v7 et traducteur	herbelin	2006-01-11
*	Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...	herbelin	2006-01-10
*	Détection var inutile par ocaml 3.09	herbelin	2006-01-10
*	Uniformisation: extension de la suppression d'un casts dans collapse_app à l...	herbelin	2005-12-21
*	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin	2005-12-17
*	Orthographe de 'instantiate'	herbelin	2005-12-17
*	j'avais oublie ces deux fichiers.	gregoire	2005-12-06
*	correction bug 881.	gregoire	2005-12-05
*	changement d'egalite pour le named_context_val	gregoire	2005-12-05
*	Changement des named_context	gregoire	2005-12-02
*	parametres inductifs	mohring	2005-11-28
*	bug #909: Top n'est cree que si le contexte est vide	barras	2005-11-23
*	petites corrections + contournement bug projections	barras	2005-11-18
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09	herbelin	2005-11-08
*	Nettoyage suite nouvel avertissement Z de ocaml 3.09	herbelin	2005-11-08
*	Types inductifs parametriques	mohring	2005-11-02
*	Suppression code inactif et commentaire apparemment incorrect (pour éviter c...	herbelin	2005-09-09
*	Simplification message d'anomalie	herbelin	2005-09-08
*	argument inutilisÃ© de zip: toujours l'identitÃ©	letouzey	2005-08-22
*	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey	2005-08-19
*	Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ...	herbelin	2005-07-21
*	reactivation de l optim des fermetures	barras	2005-07-13
*	backtrack modif de knh...	barras	2005-07-13
*	* empty log message *	barras	2005-07-13
*	test du tag de reduction	barras	2005-07-12
*	Correction bug #983	herbelin	2005-06-28
*	Bug fix for a bug reported by Roland: the function that detects the constants	sacerdot	2005-05-23
*	Bug affichage graphe univers	herbelin	2005-05-05
*	Code v7 obsolete	herbelin	2005-05-05
*	MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...	herbelin	2005-05-05
*	Moving centralised discharge into dispatched discharge_function; required to ...	herbelin	2005-02-18
*	Added map_named_context	herbelin	2005-02-18
*	Moved Indmap and ConstrMap from Libnames to Names for use in Cooking	herbelin	2005-02-18
*	Uniformisation de destApplication en destApp	herbelin	2005-02-12
*	Uniformisation de destApplication en destApp; simplification decompose_app	herbelin	2005-02-12
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	1. added code to handle the inclusion of inductive types and constructors in	sacerdot	2005-01-17
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot	2005-01-13
*	[ Waiting for a keyword to control expansion during functor application ]	sacerdot	2005-01-05
*	HUGE COMMIT	sacerdot	2005-01-03
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	Commentaire	herbelin	2004-12-06
*	* empty log message *	gregoire	2004-11-29
*	Code mort	herbelin	2004-11-22