coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Fix bug in implementation of setoid rewriting under cases and	msozeau	2010-09-27
*	Fixed a bug in printing fix/cofix error messages when several	herbelin	2010-09-24
*	Solving bug #2212 (unification under tuples now not allowed for	herbelin	2010-09-24
*	Partial review of removed dead code (r13460)	herbelin	2010-09-24
*	Checker: remove some dead code	letouzey	2010-09-24
*	Dead code in extraction	letouzey	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	dev/Makefile.oug: how to run the Oug analyser, for instance for finding dead ...	letouzey	2010-09-24
*	Added a section in the documentation of Vernacular commands about Set/Unset/T...	aspiwack	2010-09-23
*	Update CHANGES: Local/Global Set/Unset.	aspiwack	2010-09-23
*	Fix inconsistency in Prop/Set conversion check	glondu	2010-09-23
*	Report fix bug 2345 from v8.3 (Bad error message when functional	courtieu	2010-09-21
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Fixed test of bug #2360 (use of Fail to check a regular error instead	herbelin	2010-09-20
*	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey	2010-09-20
*	Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc -g") but	herbelin	2010-09-19
*	Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we	herbelin	2010-09-19
*	Reverting partial fix for #2335 committed by mistake in r13435. Sorry.	herbelin	2010-09-19
*	Hopefully a fix for #2176 (redirection not understood with some shells)	herbelin	2010-09-19
*	Addressing part 2 of bug report 2377 (removing intrusive warning when	herbelin	2010-09-19
*	Patch solving the bug but leaving open design choices	herbelin	2010-09-19
*	Fixing #2162 and #2367 (wrong order of Show Match) for branch 8.2 too	herbelin	2010-09-18
*	Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" in	herbelin	2010-09-18
*	Fixing bugs #2347 (part 2) and #2388: error message printing was done	herbelin	2010-09-18
*	Now prints an error instead of an anomaly when dynlink fails	herbelin	2010-09-18
*	Fixed a problem introduced in r12607 after pattern_of_constr served	herbelin	2010-09-17
*	In the computation of missing arguments for apply, accept that the	herbelin	2010-09-17
*	For the moment, two small manual eta-expansions to avoid '_a after extraction	letouzey	2010-09-17
*	Extraction: multiple fixes related with the Not_found encountered by X. Leroy	letouzey	2010-09-17
*	Coqdep_boot : misc improvements	letouzey	2010-09-17
*	Explicit Mod_checking signature	glondu	2010-09-16
*	Sharing is not anymore broken by traverse_module.	soubiran	2010-09-15
*	Fix likely semantic typos	glondu	2010-09-15
*	CoqIDE argv parsing delegated to coqtop	vgross	2010-09-14
*	Fix unescaped end-of-lines (OCaml warning 29)	glondu	2010-09-13
*	commit 13400 and 13409.	soubiran	2010-09-13
*	Improving a few error messages in Ltac interpretation	herbelin	2010-09-11
*	files introduce in commit 13401 aren't erased anymore by 'make clean'	pboutill	2010-09-10
*	Bugfix: A notation for a constructor where some arguments are _	pboutill	2010-09-10
*	NMake : another round of heavy rework	letouzey	2010-09-09
*	Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for png...	emakarov	2010-09-06
*	fixed bug #2375 (congruence)	corbinea	2010-09-02
*	* removed declare_constant and declare_internal_constant	vsiles	2010-09-02
*	v13392 port from v8.3 to trunk : correct message when defining inductive schemes	vsiles	2010-09-02
*	Clarified role of Set Boolean Equality Schemes wrt Set Equality Scheme +	herbelin	2010-09-02
*	Improved printing of Unfoldable constants in hints databases (used	herbelin	2010-09-02
*	* By default, load proof terms.	regisgia	2010-08-31
*	* scripts/Coqc toplevel/Usage:	regisgia	2010-08-27
*	* checker/Safe_typing.LightenLibrary:	regisgia	2010-08-27
*	* kernel/Safe_typing.LightenLibrary:	regisgia	2010-08-27