coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Better implementation of the set of instances of a given class as a Cmap	msozeau	2008-05-15
*	Various fixes:	msozeau	2008-05-15
*	really fixed Georges\' bug	barras	2008-05-15
*	Oubli lors de la révision 10899 (Bool_nat.vo)	notin	2008-05-15
*	Résolution des problèmes ambigus d'inférence du type de retour des	herbelin	2008-05-14
*	corrige le bug de Georges	barras	2008-05-14
*	- Fix bug related to indices of fixpoints.	msozeau	2008-05-13
*	debug et nouvelles commandes Dp_prelude et Dp_predefined	filliatr	2008-05-13
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	Fix "not an applied typeclass" error for legitimate classes	msozeau	2008-05-12
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
*	Changement de stratégie vis à vis du commit 10859 sur la gestion des	herbelin	2008-05-12
*	- Cleanup parsing of binders, reducing to a single production for all	msozeau	2008-05-11
*	- Changement du code de Zplus pour accomoder ring qui sinon prend une	herbelin	2008-05-11
*	Correction bug #1842 + correction bug initialisation introduit dans	herbelin	2008-05-10
*	- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des	herbelin	2008-05-10
*	Amélioration de la colorisation, du backtrack et des messages de CoqIDE	herbelin	2008-05-10
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Still Ints-->Numbers transition: fix the previous commit about a typo	letouzey	2008-05-09
*	Still Ints-->Numbers transition: fix a typo preventing the compilation of BigQ	letouzey	2008-05-08
*	Autre oubli de la révision 10904	herbelin	2008-05-08
*	remove mention of an obsolete limitation of Add Morphism	letouzey	2008-05-08