coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	Correction du bug #1679 (congruence) et ajout test-suite	corbinea	2007-09-14
*	Update before joining all signatures into one.	emakarov	2007-09-13
*	- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc	roconnor	2007-09-07
*	errors in recdef.ml4:	bertot	2007-09-06
*	this should fix a problem described in a message by Dufourd on July 30th, 2007	bertot	2007-09-06
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
*	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin	2007-09-06
*	fixed icons	barras	2007-09-04
*	fixed icons	barras	2007-09-04
*	Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte les	herbelin	2007-09-04
*	A word on the measure and wf modifiers	msozeau	2007-09-01
*	Suite commit 10103 (expansion des défs locales triviales dans l'étape	herbelin	2007-09-01
*	fin de la correction de Function	jforest	2007-08-31
*	correction bug d'efficacite dans Function	jforest	2007-08-31
*	Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server	herbelin	2007-08-30
*	Oubli dans commit 10102...	herbelin	2007-08-30
*	Prise en compte des redéfinitions de variables (définitions locales	herbelin	2007-08-29
*	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin	2007-08-29
*	Adding a few lemmas for reasoning about inequalities over the	roconnor	2007-08-28
*	Correction d'un bug dans check_and_warn	notin	2007-08-28
*	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin	2007-08-27
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	Fix bug on wellfounded defs with constant parameters and dependencies on the ...	msozeau	2007-08-26
*	Fix de Bruijn bug in wf definitions.	msozeau	2007-08-26
*	Add info on measure based defs.	msozeau	2007-08-26
*	Fix evars bug in mutual fixpoints with implicit types and bug in inequalities...	msozeau	2007-08-26
*	Add more equality tactics. Upgrade program_simpl for discrimination of conjun...	msozeau	2007-08-26
*	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin	2007-08-25
*	Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...	herbelin	2007-08-24
*	Utilisation plus précise de la contrainte de type pour interpréter les	herbelin	2007-08-24
*	Correction du bug #1634 + ajout de bugs dans la test-suite	notin	2007-08-22
*	Save IS NOT the same Defined ....	msozeau	2007-08-22
*	- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)	herbelin	2007-08-22
*	Ajout d'un warning losrqu'un nom de bibliothèque est ambigü	notin	2007-08-22
*	Modification de l'initialisation des chemins de la librairie standard	notin	2007-08-20
*	Typo in INSTALL instructions	lmamane	2007-08-20
*	Erreur de copier/coller dans la section Guarded	notin	2007-08-20
*	Correction du bug #1322	notin	2007-08-16
*	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin	2007-08-16
*	An update on axiomatic number classes.	emakarov	2007-08-13
*	Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après un...	notin	2007-08-13
*	Correction du bug #1635	notin	2007-08-13
*	Ajout d'un exemple d'inversion des dépendances dans le prédicat comme	herbelin	2007-08-10
*	- Correction d'un bug de de Bruijn dans abstract_predicate (lié au	herbelin	2007-08-10
*	Typo	notin	2007-08-10
*	Modification de la test suite pour intégrer des tests spécifiques aux	notin	2007-08-10
*	Modification de control_only_guard, qui utilise maintenant	notin	2007-08-09
*	Fix dependency bugs due to Program modules renamings.	msozeau	2007-08-08
*	Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.v	emakarov	2007-08-08