coq - The formal proof system

Age	Commit message (Expand)	Author
2007-09-04	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-01	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-08-31	fin de la correction de Function	jforest
2007-08-31	correction bug d'efficacite dans Function	jforest
2007-08-30	Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Server	herbelin
2007-08-30	Oubli dans commit 10102...	herbelin
2007-08-29	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-28	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-27	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-26	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-25	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin
2007-08-24	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-22	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-20	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-16	Correction du bug #1322	notin
2007-08-16	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin
2007-08-13	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-10	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-09	Modification de control_only_guard, qui utilise maintenant	notin
2007-08-08	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	Add a test case for the new "dependent" induction tactics.	msozeau
2007-08-08	A better Program documentation. Include it in the generated stdlib doc.	msozeau
2007-08-07	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau
2007-08-07	Add a new tactic to generalize an instantiated inductive predicate adding equ...	msozeau
2007-08-07	Build system: _really_ don't recurse into VCS metadata for file lists	lmamane
2007-08-07	Build system:	lmamane
2007-08-01	Build system: BSD compatibility: do not use -printf action of find	lmamane
2007-07-30	mul and sqrt	thery