coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	compatibility with POWERPC	gregoire	2004-11-22
*	bug module with ... + vm	barras	2004-11-17
*	bug module M:=N avec vm	barras	2004-11-17
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)	barras	2004-10-20
*	Amélioration message d'erreur objet de récursion de type non inductif	herbelin	2004-08-06
*	Nouvelle en-tête	herbelin	2004-07-16
*	correspondance des records et noms de champs de records entre un module et sa...	letouzey	2004-06-25
*	Fusion comparaison Const/Var; export is_opaque	herbelin	2004-06-02
*	Un bug résiduel (mais pas bien méchant) du noyau	herbelin	2004-05-27
*	Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...	herbelin	2004-03-28
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
*	Inductive Types : seuls les petits types sont unitaires	mohring	2003-12-19
*	bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)	barras	2003-12-16
*	* empty log message *	barras	2003-11-27
*	modif lexer: ident peut commencer par _	barras	2003-11-25
*	CC: added injection theory	corbinea	2003-11-25