coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Use COQINSTALLPREFIX for doc too	glondu	2008-07-28
*	Fix bashism in test-suite/check	glondu	2008-07-28
*	Remove pcoq from check prerequisites	glondu	2008-07-28
*	Fixes in generalize_eqs/dependent induction to allow the user to specify	msozeau	2008-07-28
*	Fix wrong environment bug in test for setoid_rewrite or rewrite.	msozeau	2008-07-28
*	Fix bug in term dnet preventing some unifications. Allow "higher-order"	msozeau	2008-07-28
*	Show configure choice for browser in CoqIDE preferences	glondu	2008-07-28
*	Now, -browser option is effective (and compiles)	glondu	2008-07-27
*	(Partially) Revert previous commit because of FTBFS	glondu	2008-07-27
*	Add -browser option to configure script	glondu	2008-07-27
*	Oups (on refait le 11268 en mieux)	herbelin	2008-07-27
*	Even better test for choosing rewrite or setoid_rewrite.	msozeau	2008-07-26
*	- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec	herbelin	2008-07-26
*	Suite 11266 (warning tools/gallina.ml)	herbelin	2008-07-25
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	Fixed bug #1904 (instances of evars were no longer substituted since	herbelin	2008-07-25
*	A better test for relations being setoids or not: do leibniz rewrite iff	msozeau	2008-07-25
*	More compatibility fixes, revert the tauto fix that prevented	msozeau	2008-07-25
*	Tauto breaking not only binary "conjunctions" seems like a bad idea	msozeau	2008-07-24
*	A (safe) implementation of prolog's cut in the typeclasses eauto to avoid	msozeau	2008-07-24
*	Fix bug #1913, checking for unresolved evars which aren't obligations.	msozeau	2008-07-24
*	fixed loop in dependency fold of the checker	barras	2008-07-24
*	moved magic numbers to configure (share coq/coqchk)	barras	2008-07-24
*	broke cyclic dependencies	barras	2008-07-24
*	Suite commit 11236	notin	2008-07-24
*	Propagation de l'information "strict" (càd à toplevel ou en train de	herbelin	2008-07-24
*	Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the	herbelin	2008-07-23
*	Stop glob messages to be printed by default on stdout	letouzey	2008-07-23
*	Oops... forgot some debug code.	msozeau	2008-07-23
*	Add test-suite file for bug# 1905 and minor fix in Program/Equality.	msozeau	2008-07-22
*	New tactics [conv] to test convertibility (actually, unification) of two	msozeau	2008-07-22
*	A try at allowing matching on applications as a binary syntax node by default.	msozeau	2008-07-22
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22
*	Oubli lors du commit #11236	notin	2008-07-22
*	Suite commit 11236	notin	2008-07-21
*	Extraction: better dependency computation (after optimisations)	letouzey	2008-07-20
*	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin	2008-07-18
*	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin	2008-07-18
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18