coq - The formal proof system

Age	Commit message (Expand)	Author
2007-10-24	Bugfix in abstract_generalize	msozeau
2007-10-24	Doc update	msozeau
2007-10-24	Fix some bugs, add possibility of automatically solving a proof statement's o...	msozeau
2007-10-23	Enlevé les trucs commités au mauvais endroit	aspiwack
2007-10-23	Quelques structures de donnée plus les modules principaux (et	aspiwack
2007-10-23	Added "is_empty" to gmap.	aspiwack
2007-10-23	Ajout de mots clés pour Coqdoc (bug #1732)	notin
2007-10-23	Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu...	emakarov
2007-10-22	Corrections des bugs #1730 et #1731	notin
2007-10-21	An error message instead of an empty extraction when the monolithic	letouzey
2007-10-21	Avoid the auto-inlining of small fixpoints like List.map.	letouzey
2007-10-21	Cleanup attempt of Hints in *Interface.v files.	letouzey
2007-10-19	Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le	roconnor
2007-10-18	Intallation des .cma/.cmxa	notin
2007-10-18	Changed RingMicromega to use NRing instead of Ring_polynom. NRing is a versio...	emakarov
2007-10-18	Copie de PreOmega.vo dans le répertoire d'installation de Coq	notin
2007-10-18	Copie des .cma et des .cmxa, et de grammar.cma dans le répertoire de Coq (po...	notin
2007-10-18	Typo dans Makefile.common	notin
2007-10-18	Report de la révision #10197 (adaptation à Lablgtk 2.10.0)	notin
2007-10-18	Uniformisation de l'option -where de coqc avec celle de coqtop	notin
2007-10-18	added generation from trivial patterns for congruence	corbinea
2007-10-17	Repair Haskell/Scheme extraction in the new extraction backend design:	letouzey
2007-10-17	Major reorganisation of the extraction "backend".	letouzey
2007-10-17	Prise en compte des .glob par coq_makefile	notin
2007-10-16	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-15	build system: When using GOTO_STAGE, always go into that stage, even when tar...	lmamane
2007-10-12	- 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-11	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-10	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-09	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-08	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