coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
*	* toplevel/Coqtop: Reactivate -dont-load-proofs option.	regisgia	2010-08-27
*	* library/Library: Reformulate a comment.	regisgia	2010-08-27
*	* library/Library: Document.	regisgia	2010-08-27
*	* checker/SafeTyping kernel/SafeTyping:	regisgia	2010-08-27
*	* lib/Flags: Replace dont_load_proofs by load_proofs since not loading	regisgia	2010-08-27
*	* Improve documentation of LightenLibrary.	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing: New LightenLibrary.	regisgia	2010-08-27
*	* library/Library: Remove the use of the old-fashioned lighten_library.	regisgia	2010-08-27
*	* library/Library: Remove lighten_library definition.	regisgia	2010-08-27
*	Fix an error message ot having the ERror: prefix.	courtieu	2010-08-26
*	Export printing functions for extra arguments. Maybe there's a way to	msozeau	2010-08-03
*	Fix [clenv_missing] to compute a better approximation of missing	msozeau	2010-08-02
*	Fixed commit r13359 which was incomplete for its "trunk" part. Thanks	herbelin	2010-07-31
*	adpated the checker to handle coomutative cuts and lazyness	barras	2010-07-30
*	Removed information in COMPATIBILITY that were intended before all for	herbelin	2010-07-30
*	better fix to bug #2319: types are compiled in the env of the bodies	barras	2010-07-30
*	Updated test on Nsatz after Loïc moved NsatzR to Nsatz.	herbelin	2010-07-30
*	Capitulation wrt "change pat with term": instead of solving the	herbelin	2010-07-30
*	r13359 continued: removed native treatment for λ (lambda) and Π (Pi)	herbelin	2010-07-30
*	Rather quick hack to make basic unicode notations available by	herbelin	2010-07-29