coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Prise en compte des .glob par coq_makefile	notin	2007-10-17
*	add visibility of extraction messages in coqide	letouzey	2007-10-16
*	Correction d'un bug de l'appel à make via Coqide	notin	2007-10-16
*	Fixed congruence instance generator + changed default depth to 1000	corbinea	2007-10-16
*	Added transitivity and irreflexivity of <, as well as < -elimination for bina...	emakarov	2007-10-16
*	Added the doc for the new Scheme Equality command	vsiles	2007-10-16
*	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin	2007-10-16
*	build system: When using GOTO_STAGE, always go into that stage, even when tar...	lmamane	2007-10-15
*	- Préservation des appels récursifs de tête dans ltac (réponse au "wish"	herbelin	2007-10-12
*	Uniformisation du comportement de rewrite et rewrite in : quand le	herbelin	2007-10-12
*	Maj du lien vers coq-bugs dans Coqide	notin	2007-10-12
*	Allow a few build system optimisations/corner-cutting	lmamane	2007-10-11
*	Bug variable CAMLP4 qui ne doit pas contenir un chemin mais le type de prepro...	herbelin	2007-10-11
*	Allowing setoid_reflexivity_in to work on quantified hypothesis (bug #1710)	letouzey	2007-10-10
*	Mise à jour des notes d'installation pour Coqide	notin	2007-10-10
*	Ajout d'une note sur Ocaml 3.10.0 et camlp5	notin	2007-10-10
*	Extraction now checks that the required libraries are indeed loaded (bug #1144)	letouzey	2007-10-09
*	forbid extraction under a module type	letouzey	2007-10-09
*	Extract Inline/Inductive/Constant can now be used from inside a module	letouzey	2007-10-09
*	Verification ocaml >= 3.09.3 pour coq natif sous MacOS X Pentium	herbelin	2007-10-09
*	Oubli de GTK pour Windows + typo	notin	2007-10-09
*	Mise à jour de README.win	notin	2007-10-09
*	Amélioration de l'appel aux outils externes via Coqide	notin	2007-10-09
*	documentation of commit 10188	letouzey	2007-10-08
*	Calcul des dependances sous Windows	notin	2007-10-08
*	Better use of tables for storing results of extract_ind (bug #1709)	letouzey	2007-10-08
*	add $COQTOP to the search path of ocamldebug	letouzey	2007-10-08
*	Détection de camlp5 5.00 au configure	herbelin	2007-10-07
*	Ajout de la possibilité de donner le chemin de la bibliothèque camlp5	herbelin	2007-10-07
*	Allowing infix constructors/types in a Extract Inductive	letouzey	2007-10-06
*	Extraction: factorisation of identical branches in a match	letouzey	2007-10-06
*	Correction du bug #1715	notin	2007-10-05
*	petite reparation de la config pour camlp5 apres le commit 10164	letouzey	2007-10-05
*	Added the automatic generation of the boolean equality if possible and the	vsiles	2007-10-05
*	Correction de quelques défauts d'affichage (notations sous "as" pour	herbelin	2007-10-05
*	Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o...	emakarov	2007-10-04
*	Ajout option -lablgtkdir au configure (basé sur patch de Guillaume	herbelin	2007-10-04
*	Bug 1716: Scheme now print the right messages	vsiles	2007-10-04
*	Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)	herbelin	2007-10-04
*	Compilation sous windows	notin	2007-10-03
*	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin	2007-10-03
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	BigZ now are proved	thery	2007-10-03
*	The following now compiles: abstract integers with plus, minus and times, bin...	emakarov	2007-10-02
*	Preventing gcc to generate dependencies wrt OCaml files (otherwise, we run in...	notin	2007-10-02
*	Fix a problem doing 'make clean' under Winodws	notin	2007-10-02
*	Report des modifications faites sur le configure en r10039, r10052, r10053 et...	notin	2007-10-02
*	Now NMake is proved	thery	2007-10-02
*	Correcting error message when adding Setoid, Relation or morphism (bug #1626)	jforest	2007-10-02
*	Added the compilation of theories/Numbers to Makefile.common. The following t...	emakarov	2007-10-01