coq - The formal proof system

Age	Commit message (Expand)	Author
2010-09-14	CoqIDE argv parsing delegated to coqtop	vgross
2010-09-13	Fix unescaped end-of-lines (OCaml warning 29)	glondu
2010-09-13	commit 13400 and 13409.	soubiran
2010-09-11	Improving a few error messages in Ltac interpretation	herbelin
2010-09-10	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-09	NMake : another round of heavy rework	letouzey
2010-09-06	Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for png...	emakarov
2010-09-02	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-08-31	* By default, load proof terms.	regisgia
2010-08-27	* 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-26	Fix an error message ot having the ERror: prefix.	courtieu
2010-08-03	Export printing functions for extra arguments. Maybe there's a way to	msozeau
2010-08-02	Fix [clenv_missing] to compute a better approximation of missing	msozeau
2010-07-31	Fixed commit r13359 which was incomplete for its "trunk" part. Thanks	herbelin
2010-07-30	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-29	Rather quick hack to make basic unicode notations available by	herbelin
2010-07-29	Fixed a bug introduced (r13316/r13329) in the printing of notations	herbelin
2010-07-29	kernel conversion and reduction do not raise assert failure on ill-typed term...	barras
2010-07-29	test-case for bug #2105	barras
2010-07-29	fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...	barras
2010-07-29	fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...	barras
2010-07-28	Fix bug #2209, don't use the fragile argument name "y" to pass the	msozeau
2010-07-28	Rewrite Heap merging so that it extracts to an O(n log n) definition.	msozeau
2010-07-28	unification des tactiques nsatz pour R Z avec celle des anneaux integres	pottier
2010-07-28	oops. commited files I shouldn't have. reverting on r13341	barras
2010-07-28	ported r13340 to trunk	barras
2010-07-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...	pottier