coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A slightly more efficient test of well-typedness of restriction of	herbelin	2013-02-21
*	Added propagation of evars unification failure reasons for better	herbelin	2013-02-17
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Fixed bug #2981 (anomaly NotASort in Retyping due to collision between	herbelin	2013-02-05
*	Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).	herbelin	2013-01-29
*	Added a file for testing regression of bug #2955 (anomaly in simpl in	herbelin	2013-01-29
*	Fixing bug #2969 (admit failing after Grab Existential Variables due	herbelin	2013-01-29
*	Fixed bug #2966 (de Bruijn error in computation of heads for coercions).	herbelin	2013-01-28
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fixing one part of #2830 (anomaly "defined twice" due to nested calls to	herbelin	2013-01-28
*	Fix bug 2958: Inductive deep in in clause are impossible	pboutill	2013-01-21
*	Last test-suite not in Symmetric Patterns syntax	pboutill	2013-01-21
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	Fixing parsing of specific primitive tokens used as notations for patterns	herbelin	2012-12-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
*	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