coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Backtrack on activating scopes with type casts (was r15978).	herbelin	2012-12-04
*	Revised the strategy for automatic insertion of spaces when printing	herbelin	2012-12-04
*	Evarconv: Fix #2936 + comments	pboutill	2012-11-28
*	Fixed bug #2930: folded let-in's were hiding a violation to the occur	herbelin	2012-11-25
*	Fixing test-suite: Scope.v	ppedrot	2012-11-21
*	Hurkens' paradox on Type (r15973 and r15977) needs two (non-Set)	herbelin	2012-11-18
*	Update output/Search.out after hint-related extra defs in Peano	letouzey	2012-11-17
*	Taking into account the type of a definition (if it exists), and the	herbelin	2012-11-17
*	Fix test-suite output/* in bench	pboutill	2012-10-17
*	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