coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Improve typeclasses eauto using the dnet for local assumptions too, and select	msozeau	2008-09-04
*	Correction du bug #1937	notin	2008-09-04
*	Rely on ocamlc to call the C compiler...	glondu	2008-09-04
*	Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving an	msozeau	2008-09-04
*	Better handling of recursive Equations definitions... still not perfect.	msozeau	2008-09-03
*	Fix bug #1935, reworking the reflexivity, symmetry... tactics to use	msozeau	2008-09-03
*	Correct handling of implicit arguments in [Equations] definitions,	msozeau	2008-09-03
*	Add support for recursive definitions to [Equations], deciding if a	msozeau	2008-09-02
*	Initial implementation of a new command to define (dependent) functions by	msozeau	2008-09-02
*	- Remove some dead code in subtac	msozeau	2008-09-02
*	fixed minor environment issues when checking inductive types	barras	2008-09-02
*	fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...	barras	2008-09-02
*	added Makefile target: validate (to recheck all .vo in a row)	barras	2008-09-02
*	avoid small overflows	barras	2008-09-02
*	[checker] basic conversion oracle: expand local vars first	barras	2008-09-02
*	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin	2008-09-02
*	Fix implementation of "Global Instance" which redeclared the same	msozeau	2008-08-27
*	Major speed and space improvements in setoid rewrite:	msozeau	2008-08-27
*	Little cleanup in auto.	msozeau	2008-08-27
*	Give back progress information after feeding the Program Instance to the	msozeau	2008-08-26
*	Fix dependency problem that makes compilation fail :)	msozeau	2008-08-23
*	- New auto hints for transparency/opacity control, not bound to	msozeau	2008-08-22
*	Typo (corrige le bug #1928)	notin	2008-08-22
*	Fixes in dependent induction tactic to keep names, allow giving	msozeau	2008-08-21
*	Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside	msozeau	2008-08-21
*	Revert commit 11326, to see if it is what makes bench fail	glondu	2008-08-18
*	Renaming parser -> coq-parser	glondu	2008-08-18
*	Install csdpcert with libraries	glondu	2008-08-16
*	Mind environment variables in (generated) coq_config.ml	glondu	2008-08-16
*	Fix build/install failures when ocamlopt is not available	glondu	2008-08-16
*	Add coqide manpage (taken from Debian)	glondu	2008-08-12
*	Various fixes in manpages	glondu	2008-08-08
*	Suite commit #11311	notin	2008-08-07
*	micromega : bug fixes and optimisations	fbesson	2008-08-07
*	eviter redondance du message d'erreur (Error while reading / File)	barras	2008-08-07
*	coqc: warning de l'option -dump-glob (unused case)	barras	2008-08-07
*	Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppressi...	notin	2008-08-06
*	Add lemmas on lists: nth_default_eq, map_nth_error	glondu	2008-08-06
*	correction : coqart is already published	jnarboux	2008-08-06
*	Correction de bugs:	herbelin	2008-08-05
*	Correction bug de filtrage sous-terme #1920 introduit dans commit	herbelin	2008-08-05
*	Suite 11187 et 11298 : ne retarder le dépliage d'une projection	herbelin	2008-08-05
*	Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par	herbelin	2008-08-04
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Corrige un bug du commit 11187 (le comportement à respecter était	herbelin	2008-07-31
*	Oops... the trunk behaviour is different	glondu	2008-07-29
*	Update test-suite output	glondu	2008-07-29
*	Typo in doc	glondu	2008-07-29
*	Backport r11289.	msozeau	2008-07-29
*	Fix typo	glondu	2008-07-28