coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	test for apply + TC resolution	Enrico Tassi	2014-03-26
*	Pos.compare_cont takes the comparison as first argument	Pierre Boutillier	2014-02-28
*	Add a test suite file for Ltac's "+" tactical.	Arnaud Spiwack	2014-01-06
*	Remove duplicate test-suite file.	Arnaud Spiwack	2013-12-06
*	Fix the refine related test-suite files to account for the new refine.	Arnaud Spiwack	2013-12-06
*	Fixing some tests from the test-suite.	ppedrot	2013-09-03
*	* test-suite/success/Unicode_utf8:	regisgia	2013-09-02
*	More dynamic argument scopes	letouzey	2013-07-17
*	Continuing r16621 on injection intro-patterns:	herbelin	2013-07-10
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Fix [setoid_rewrite] forgetting some evars that are produced when typecheckin...	msozeau	2013-06-10
*	Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an	herbelin	2013-06-02
*	Fixing a regression in unification introduced in r16205 (error raised	herbelin	2013-05-14
*	A uniformization step around understand_* and interp_* functions.	herbelin	2013-05-09
*	Declaration of multiple hypotheses or parameters now share typing	herbelin	2013-05-08
*	Share more information between constructors and arity of an inductive	herbelin	2013-05-08
*	Moved isolated test params_ind.v to Inductive.v.	herbelin	2013-05-08
*	Hack to solve a "Bad recursive type" anomaly.	herbelin	2013-05-05
*	Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.	herbelin	2013-03-21
*	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin	2013-03-21
*	Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).	herbelin	2013-01-29
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fix bug 2958: Inductive deep in in clause are impossible	pboutill	2013-01-21
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Taking into account the possibility of having a type of type which is	herbelin	2012-12-18
*	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin	2012-12-18
*	Backtrack on activating scopes with type casts (was r15978).	herbelin	2012-12-04
*	Evarconv: Fix #2936 + comments	pboutill	2012-11-28
*	Fixing test-suite: Scope.v	ppedrot	2012-11-21
*	Taking into account the type of a definition (if it exists), and the	herbelin	2012-11-17
*	test-suite: Local Tactic Notation is now legal since r15731	letouzey	2012-08-23
*	Unification in Evar_conv uses an abstract machine state	pboutill	2012-08-09
*	Updating headers.	herbelin	2012-08-08
*	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
*	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 #2809 (anomaly when printing a module with notations due to	herbelin	2012-06-20
*	Proof using: nested sections bugfix	gareuselesinge	2012-06-18
*	Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.	ppedrot	2012-06-12
*	Repair two tests	letouzey	2012-04-12
*	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