coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey	2011-01-28
*	Make simpl use the proper constant when folding (mutual) fixpoints	letouzey	2011-01-27
*	Rewrite sort_universes to minimize the number of universes	glondu	2011-01-25
*	In univ.ml, put universe_level primitives in its their own sub-module	glondu	2011-01-11
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	More coherent comment ordering	glondu	2011-01-11
*	Fixing bug #2454: inversion predicate strategy for inferring the type	herbelin	2010-12-19
*	Univ: try to avoid a few lookup in the universe graph	letouzey	2010-12-18
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Revert last commit 13723 on Univ : minor gains and more complex code	letouzey	2010-12-18
*	Univ: an attempt to lazily compact chains of Equiv in a functionnal way	letouzey	2010-12-17
*	Univ: two improvements (speed + space)	letouzey	2010-12-16
*	* Kernel/Term:	regisgia	2010-12-01
*	* Kernel/Term	regisgia	2010-12-01
*	* Kernel/Term	regisgia	2010-12-01
*	Minor fixes from Gregory Malecha. A typo fixed and a better (located)	msozeau	2010-11-15
*	Correction bug 2427	soubiran	2010-11-03
*	Remove suspiciously named "implicit" stuff from Term	glondu	2010-11-03
*	In Univ, unify order_request and constraint_type	glondu	2010-11-03
*	More generic Univ.dump_universes	glondu	2010-11-02
*	Reintroduce kind_of_type (used by Presburger contrib)	glondu	2010-10-05
*	Forgotten lifts in eta-expansion	glondu	2010-10-04
*	Fixing printing of module_path names (was using a debugging	herbelin	2010-10-03
*	Remove kind_of_type, kind_of_term2 (dead code)	glondu	2010-09-28
*	Partial review of removed dead code (r13460)	herbelin	2010-09-24
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Fix inconsistency in Prop/Set conversion check	glondu	2010-09-23
*	Added eta-expansion in kernel, type inference and tactic unification,	herbelin	2010-09-20
*	Sharing is not anymore broken by traverse_module.	soubiran	2010-09-15
*	Fix likely semantic typos	glondu	2010-09-15
*	* kernel/Safe_typing.LightenLibrary:	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing:	regisgia	2010-08-27
*	* checker/SafeTyping kernel/SafeTyping:	regisgia	2010-08-27
*	* Improve documentation of LightenLibrary.	regisgia	2010-08-27
*	* (checker\|kernel)/Safe_typing: New LightenLibrary.	regisgia	2010-08-27
*	better fix to bug #2319: types are compiled in the env of the bodies	barras	2010-07-30
*	kernel conversion and reduction do not raise assert failure on ill-typed term...	barras	2010-07-29
*	fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...	barras	2010-07-29
*	ported r13340 to trunk	barras	2010-07-28
*	fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies	barras	2010-07-28
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	fixed (serious) bug #2353: non-recursive parameters of nested inductive types...	barras	2010-07-16
*	removed a potentially dangerous try ... with _ -> ...	barras	2010-07-16
*	Mod_typing: fix the content of the typ_expr_alg field	letouzey	2010-07-07
*	Names: remove obsolete mod_self_id	letouzey	2010-06-23
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin	2010-06-14
*	Fixing spelling: pr_coma -> pr_comma	herbelin	2010-06-12