coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Finer fix for bug 3017, mark unresolvability only of goals that are	msozeau	2013-04-18
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	Using Parameter instead of Variable in test-suite/output	herbelin	2013-04-17
*	Like in r16346, do not filter local definitions (here in the	herbelin	2013-04-17
*	Added regression test for bug #3023 which was solved by Matthieu's	herbelin	2013-04-16
*	Equality: avoid some unprotected List.nth (fix #2837)	letouzey	2013-04-10
*	Enrich test-suite with a test for #3022.	ppedrot	2013-04-08
*	Continuation of r16346 on filtering local definitions. Refined	herbelin	2013-03-30
*	Enrich test-suite with a test for #2928	letouzey	2013-03-25
*	Enrich test-suite with a test for #2734	letouzey	2013-03-25
*	Add the test-case of bug 2750 in the test-suite	letouzey	2013-03-25
*	Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.	herbelin	2013-03-21
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Firstorder: record with defined field aren't conjonctions (fix #2629)	letouzey	2013-03-21
*	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin	2013-03-21
*	Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)	letouzey	2013-03-21
*	Check a list length before doing a List.chop (fix #3000)	letouzey	2013-03-20
*	Fix for bug #3004 (thanks Hugo!)	letouzey	2013-03-18
*	Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...	pboutill	2013-02-25
*	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