coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix compilation and test-suite of nsatz	glondu	2010-07-12
*	nsatz in an integral domain with specialization to Z and R	pottier	2010-07-08
*	Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.	msozeau	2010-06-30
*	Made tclABSTRACT normalize evars before saying it does not support	herbelin	2010-06-29
*	Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.	herbelin	2010-06-26
*	Restored a "feature" of unification in pre-8.3 (it was used e.g. in a	herbelin	2010-06-25
*	Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)	letouzey	2010-06-20
*	Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).	herbelin	2010-06-18
*	add in test-suite the scripts about fsetdec bugs	letouzey	2010-06-18
*	test for bug #2141 (include + extraction)	letouzey	2010-06-16
*	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin	2010-06-14
*	Fixing bug 2295 (omission of option "as" in return clause of "match" was not	herbelin	2010-06-13
*	Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).	herbelin	2010-06-13
*	Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem with	herbelin	2010-06-13
*	Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"	herbelin	2010-06-13
*	Fixed bug #2314 (inversion using not checking the correctness of its arguments	herbelin	2010-06-13
*	Fixed bug #2135 (second-order unification was raising cryptic message)	herbelin	2010-06-12
*	Added regression tests for bugs + miscellaneous improvements	herbelin	2010-06-12
*	Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).	herbelin	2010-06-11
*	Fixed bug # 2303 in r 13087.	msozeau	2010-06-09
*	Fix bug #2262: bad implicit argument number by avoiding counting	msozeau	2010-06-09
*	Automatic introduction of names given before ":" in Lemma's and	herbelin	2010-06-09
*	Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.	herbelin	2010-06-09
*	Added support for Ltac-matching terms with variables bound in the pattern	herbelin	2010-06-06
*	Backported r13068 to branch v8.3 (whd_betaiota on inferred return	herbelin	2010-06-04
*	Grobner.v removed	pottier	2010-06-04
*	plugin groebner updated and renamed as nsatz; first version of the doc of nsa...	pottier	2010-06-03
*	Fix xml test in non-local mode	glondu	2010-06-02
*	Fix test-suite cleaning	glondu	2010-06-02
*	Introducing strong typing for IDE - toplevel IPC	vgross	2010-05-31
*	A little bit of cleanup, and some annotations.	fkirchne	2010-05-28
*	Added examples for checking that the guard condition excludes subterms	herbelin	2010-05-20
*	Fix bug 2307	pboutill	2010-05-20
*	fixed guard check with commutative cuts	barras	2010-05-20
*	Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.	herbelin	2010-05-10
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Disable ideal-features tests by default	glondu	2010-04-26
*	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
*	Fixed some printing bugs.	herbelin	2010-04-18
*	Moved Case3.v from ideal features to success (it works since 8.2).	herbelin	2010-04-17
*	Remove only *.v.log files in clean of test-suite/Makefile	glondu	2010-04-13
*	Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").	herbelin	2010-04-11
*	Prettier test-suite/Makefile	glondu	2010-04-10
*	Optimized need for delimiters when disjoint scopes for strings and	herbelin	2010-04-10
*	Use the Makefile in test-suite/check	glondu	2010-04-10
*	Makefile for the test-suite	glondu	2010-04-10
*	Fix typos in test-suite script	glondu	2010-04-10
*	Test for bug #2231 (unexpected error when using let/if over an inductive	herbelin	2010-04-10