coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réorganisation des points d'appui du undo de CoqIDE (type reset_info).	herbelin	2008-05-26
*	Encore un bug de undo	herbelin	2008-05-26
*	Résolution bug #1850 sur notations avec niveaux inconnus de	herbelin	2008-05-26
*	Fix bashism in doc generation.	glondu	2008-05-26
*	Bug undo CoqIDE sur End	herbelin	2008-05-26
*	the -g option is not recongnized in ocaml < 3.10.0	jforest	2008-05-26
*	- Nouvelle option "Set Printing Existential Instances" pour forcer	herbelin	2008-05-25
*	- Prise en compte des frozen state de Coq autant que possible pour	herbelin	2008-05-24
*	Ajout de la possibilité d'utiliser fix/cofix dans les notations.	herbelin	2008-05-24
*	doc of coqchk + improved module cache and computation of module sets	barras	2008-05-23
*	Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...	letouzey	2008-05-23
*	- Fix bug #1858, Hint Unfold calling the wrong locate function.	msozeau	2008-05-23
*	Nouvelle doc pour les modules.	soubiran	2008-05-23
*	(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...	letouzey	2008-05-23
*	Strategy commands are now exported	barras	2008-05-22
*	fixed dependency problems with the checker	barras	2008-05-22
*	writing a match on a digit via syntax "if ... then ... else" is not a good id...	letouzey	2008-05-22
*	Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...	letouzey	2008-05-22
*	QRewrite is now obsolete. It was containing manual ltac stuff	letouzey	2008-05-22
*	Should fix the dependancy issue mentioned by J.Forest about NMake:	letouzey	2008-05-22
*	switch theories/Numbers from Set to Type (both the abstract and the bignum pa...	letouzey	2008-05-22
*	improved coqchk targets	barras	2008-05-22
*	added coqchk to the main Makefile and a make variable VALIDATE to check the v...	barras	2008-05-22
*	refined the conversion oracle	barras	2008-05-21
*	refined the conversion oracle	barras	2008-05-21
*	Désactivation affichage image coqide en attendant un barcelos	herbelin	2008-05-21
*	Correction bugs ide undo et highlight (suite à typos)	herbelin	2008-05-21
*	Correction d'un bug de l'unification pattern qui oubliait d'expanser	herbelin	2008-05-20
*	Corrections d'erreurs rapportées par Frédéric Besson sur le précédent	herbelin	2008-05-20
*	added checker to svn:ignore	barras	2008-05-20
*	also fixed conversion of the checker	barras	2008-05-20
*	Cleanup build_new, remove unneeded try-with and debug interaction of	msozeau	2008-05-20
*	Léger backtrack sur commit coqide précédent (si la commande à annuler	herbelin	2008-05-20
*	Fixed coqide bug #1856 that was introduced in revision 10915.	herbelin	2008-05-20
*	Retrait d'un test commité par erreur en 10947	herbelin	2008-05-20
*	MAJ crédits	herbelin	2008-05-19
*	Intégration de micromega ("omicron" pour fourier et sa variante sur Z,	herbelin	2008-05-19
*	Fix globalization bug in class_tactics and refactorize instance	msozeau	2008-05-19
*	Fix caml debug flags configuration, -g works with the native compiler only	msozeau	2008-05-19
*	Minor improvement: group stuff about carry apart from stuff about zn2z	letouzey	2008-05-19
*	Thanks to Matthieu's commit 10941, Ad-hoc tactics contained in QRewrite are n...	letouzey	2008-05-19
*	ZModulo: Z viewed modulo 2^digits implements CyclicAxioms	letouzey	2008-05-17
*	Fix a de Bruijn bug in setoid_rewrite when rewriting under	msozeau	2008-05-17
*	Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurate	letouzey	2008-05-16
*	BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZ	letouzey	2008-05-16
*	Deletion of empty directory TreeMod	letouzey	2008-05-16
*	ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.	letouzey	2008-05-16
*	More BigNum cleanup:	letouzey	2008-05-16
*	In practice, the new setoid rewrite (and the "at" syntax) allows to avoid	letouzey	2008-05-15
*	Coq headers + $ in theories/Numbers files	letouzey	2008-05-15