coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	test-suite: fix grep rule for output tests	pboutill	2012-09-04
*	test-suite uses coqtop instead of coqtop.byte	pboutill	2012-09-04
*	In the output tests, ignore dynlink messages	letouzey	2012-08-24
*	test-suite: Local Tactic Notation is now legal since r15731	letouzey	2012-08-23
*	No more coqtop.opt, produce directly a coqtop binary	letouzey	2012-08-23
*	Unification in Evar_conv uses an abstract machine state	pboutill	2012-08-09
*	Updating headers.	herbelin	2012-08-08
*	Fixing #2836 (materialize_evar might refine as a side effect the	herbelin	2012-07-29
*	Fixing bug #2835 (the rationale for printing notations was not	herbelin	2012-07-21
*	Improving management of notations with binders (see #2708 where a	herbelin	2012-07-21
*	Restore test file induct.v where the "in \|- *" is mandatory	letouzey	2012-07-10
*	Continuing r15459: it helps testing occur-check early in some	herbelin	2012-07-06
*	Minor fixes in the test-suite after my recent commits	letouzey	2012-07-06
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Fixing bug #2817 (occur check was not done up to instantiation of	herbelin	2012-06-20
*	Fixing bug #2809 (anomaly when printing a module with notations due to	herbelin	2012-06-20
*	Proof using: nested sections bugfix	gareuselesinge	2012-06-18
*	Constrextern is allow to use partially applied notations	pboutill	2012-06-14
*	Fixing test-suite after last storm in Pp.	pboutill	2012-06-12
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
*	Notations are back in the "in" clause of pattern matching.	pboutill	2012-05-15
*	Implicit arguments of Definition are taken from the type when given by the user.	pboutill	2012-04-27
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
*	Bug 2733 : { } implicits and Fixpoints	pboutill	2012-04-17
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Repair two tests	letouzey	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Relax uniform inheritance condition	gareuselesinge	2012-04-05
*	Unification: Added a heuristic to solve problems of the form	herbelin	2012-03-26
*	Fix the test-suite by removing any Reset in the scripts	letouzey	2012-03-23
*	evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structures	gareuselesinge	2012-03-22
*	Fixing bug #2724 (using notations with binders in cases patterns	herbelin	2012-03-20
*	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin	2012-03-20
*	Generalized the use of evar candidates in type inference unification:	herbelin	2012-03-20
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Fixing bug #2732 (anomaly when using the tolerance for writing	herbelin	2012-03-18
*	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin	2012-03-13
*	"Let in" in pattern hell, one more iteration	pboutill	2012-03-02
*	Noise for nothing	pboutill	2012-03-02
*	Use a heuristic to not simplify equality hypotheses remaining after dependent...	msozeau	2012-02-20
*	Arguments supports extra notation scopes	gareuselesinge	2012-02-14
*	Fix consequence of pp bugfix in testsuite	pboutill	2012-01-31
*	Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...	msozeau	2012-01-28
*	Notations with binders: Accepting using notations for functional terms	herbelin	2012-01-20
*	Parameters in pattern first step.	pboutill	2012-01-16
*	Add distclean back to test-suite/Makefile	glondu	2012-01-14
*	Backtracking on r14876 (fix for bug #2267): extra scopes might be	herbelin	2012-01-05