coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.	herbelin	2010-05-10
*	Fix: Pfedit.get_current_goal_context when no goal is focused.	aspiwack	2010-05-10
*	Removed an evar_merge in clenv_fchain which not only is incorrect but	herbelin	2010-05-10
*	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
*	Update of credits files	herbelin	2010-05-09
*	Fix bug #2315 : printing of defined evars in Coqide.	aspiwack	2010-05-07
*	Deux commentaires retirés de ocamldoc.	aspiwack	2010-05-07
*	better detection of nested recursion in Function	jforest	2010-05-07
*	Correction of a bug pointed by P. Casteran.	jforest	2010-05-07
*	Trying to find a problem pointed by P. Casteran	jforest	2010-05-07
*	term matching in ltac was not coherent with match goal in presence of wildcar...	jforest	2010-05-06
*	Correction in Function documentation	jforest	2010-05-06
*	Patch bug 2313.	soubiran	2010-05-05
*	Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proof	pboutill	2010-05-05
*	- Fixing bug #2308 about Lemma ... with	vsiles	2010-05-04
*	Correction of bug 2290 (removing stupid message)	jforest	2010-05-04
*	Correction of bug 2290	jforest	2010-05-04
*	ocamldoc related fixes	pboutill	2010-05-03
*	Re-enable validation in "make check", run it in parallel with test-suite	glondu	2010-05-03
*	Fix discrimination of sorts which doesn't play well with cumulativity	msozeau	2010-05-02
*	Extraction: fix type_expunge_from_sign broken in last commit	letouzey	2010-05-01
*	Extraction: an experimental command to get rid of some cst/constructor arguments	letouzey	2010-04-30
*	Fail: a way to check that a command is refused without blocking a script	letouzey	2010-04-30
*	"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
*	Two forgotten $Id$ in last commit	letouzey	2010-04-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Removed obsolete v7->v8 translation code (function check_same_type is	herbelin	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Dont recompute the contents of the proof window when entering the	vgross	2010-04-28
*	Fix bug #2245, incorrect handling of Context in sections inside module	msozeau	2010-04-27
*	small detail about Scheme Equality	vsiles	2010-04-27
*	Added a new exception for already declared Schemes,	vsiles	2010-04-27
*	Misc small fixes : warning, dep cycles, ocamlbuild...	letouzey	2010-04-26
*	Disable ideal-features tests by default	glondu	2010-04-26
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin	2010-04-22
*	Ignore *.stamp files	herbelin	2010-04-22
*	Fixed bugs from commit 12954 on unification complexity	herbelin	2010-04-20
*	missing space in error message	vsiles	2010-04-20
*	Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)	herbelin	2010-04-20
*	Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2	herbelin	2010-04-20
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
*	In function "substitution_prefixed_by" the prefix test on module path	soubiran	2010-04-19
*	Fixed some printing bugs.	herbelin	2010-04-18
*	A pass on the CHANGES file + credits for 8.3 (completing commit 12906	herbelin	2010-04-17
*	Moved Case3.v from ideal features to success (it works since 8.2).	herbelin	2010-04-17