coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	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-08
*	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-07
*	Build system: BSD compatibility: do not use -printf action of find	lmamane	2007-08-01
*	mul and sqrt	thery	2007-07-30
*	Corrected the reference to glob.dump, which is used to create stdlib/index-bo...	emakarov	2007-07-26
*	Add glob.dump to Makefile the recommended way and document the	lmamane	2007-07-25
*	Modifications de la construction de la documentation de la librairie	notin	2007-07-25
*	Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n et	notin	2007-07-25
*	fixed bug 1448 and 1674	barras	2007-07-24
*	proof of compare added	thery	2007-07-24
*	fixed bug 1675: computing carrier from the relation type was not right	barras	2007-07-24
*	Declarative language: fixed the generation of fixpoints for induction proofs.	corbinea	2007-07-24
*	An update on axiomatization of numbers.	emakarov	2007-07-24
*	removed thesis	barras	2007-07-23
*	Documentation of Program and its tactics, fix enormous interaction bug due to...	msozeau	2007-07-19
*	some more svn:ignore properties	letouzey	2007-07-19
*	A generic preprocessing tactic zify for (r)omega	letouzey	2007-07-18
*	Makefile: slightly cleaner version of r10026	lmamane	2007-07-18