coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	"Improved" the form of the inferred type of "match" by	herbelin	2010-06-03
*	fixed guard check with commutative cuts	barras	2010-05-20
*	Mrec was not substituted correctly	barras	2010-05-20
*	Discontinue support for ocaml 3.09.*	letouzey	2010-05-19
*	Some ocamldoc comments + Fixing name of .coqrc.version file in refman	pboutill	2010-05-18
*	Applicative commutative cuts in Fixpoint guard condition	pboutill	2010-05-18
*	Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)	herbelin	2010-05-09
*	Added a few informations about file lineages (for the most part in kernel)	herbelin	2010-05-09
*	"make source-doc" builds documentation of mli in html and pdf at	pboutill	2010-04-29
*	After the approval of Bruno, here the patch for the checker.	soubiran	2010-04-29
*	Various minor improvements of comments in mli for ocamldoc	letouzey	2010-04-29
*	fixed bug #2224 (Error message in positivity check fixed)	vsiles	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)	herbelin	2010-04-20
*	In function "substitution_prefixed_by" the prefix test on module path	soubiran	2010-04-19
*	cf. 12945	soubiran	2010-04-16
*	Names.mli: double declaration of mind_modpath	letouzey	2010-04-16
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	introduced lazy computation of size info in the guard condition	barras	2010-03-11