coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\
\| *	Fixing output test Notations2.	Hugo Herbelin	2016-04-22
\| *	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
* \|	A small test of Print Ltac.	Hugo Herbelin	2016-04-09
* \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\| \|
\| * \|	Fix test suite after change in extraction.	Maxime Dénès	2015-12-15
* \| \|	Using x in output test-suite Cases.v (cosmetic).	Hugo Herbelin	2015-12-05
* \| \|	Fixing output test Cases.v.	Pierre-Marie Pédrot	2015-11-15
* \| \|	Updating test-suite after Bracketing Last Introduction Pattern set by	Hugo Herbelin	2015-11-10
* \| \|	Merge origin/v8.5 into trunk	Hugo Herbelin	2015-11-10
\|\\| \|
* \| \|	Adapting output test inference.v after c23f0cab6 (experimenting	Hugo Herbelin	2015-11-08
\| * \|	Fixing output test Existentials.v after eec77191b.	Hugo Herbelin	2015-11-07
\|/ /
* \|	Fixing a bug in reporting ill-formed inductive.	Hugo Herbelin	2015-10-22
* \|	Fixing test-suite	Hugo Herbelin	2015-10-11
* \|	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
* \|	Refining 0c320e79ba30 in fixing interpretation of constr under binders	Hugo Herbelin	2015-10-11
* \|	Test for bug #4269.	Pierre-Marie Pédrot	2015-09-15
* \|	Update test-suite after 518049fe7.	Maxime Dénès	2015-09-03
\| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\|/
*	Output test for bug #2169.	Pierre-Marie Pédrot	2015-07-27
*	Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.	Maxime Dénès	2015-06-24
*	Do not display the status of monomorphic constants unless in universe-polymor...	Guillaume Melquiond	2015-03-09
*	Fix testsuite with respect to the new formatting of Fail messages.	Guillaume Melquiond	2015-03-05
*	Undo: back to 8.4 semantics (Close #3514)	Enrico Tassi	2015-02-15
*	Fixing name of evars in output test Notation.v.	Hugo Herbelin	2015-01-12
*	Adapted test file for About.	Pierre Courtieu	2014-12-15
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Tests for Searchxxx commands added and modified.	Pierre Courtieu	2014-12-15
*	Adapting output tests to current naming of evars, even if unclear	Hugo Herbelin	2014-11-11
*	Consequence of changing the definition of Nat.shiftl and Nat.shiftr.	Hugo Herbelin	2014-11-06
*	Fixing clash in output test-suite Cases.	Hugo Herbelin	2014-10-23
*	Taking into account factorization of consecutive names of same types	Hugo Herbelin	2014-10-23
*	Fixing typo in output test Notations.	Hugo Herbelin	2014-10-22
*	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin	2014-10-21
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Adapting output/Arguments_renaming continued.	Hugo Herbelin	2014-10-03
*	An evar name changed in output test.	Hugo Herbelin	2014-10-02
*	Adapting the output test Notations:	Hugo Herbelin	2014-10-02
*	Revert "test-suite: New names for vars but the expected invariant is preserved"	Hugo Herbelin	2014-10-02
*	Adapting output/Arguments_renaming.out after fixing printing of	Hugo Herbelin	2014-10-02
*	Adapting to naming of evars.	Hugo Herbelin	2014-09-27
*	Reductionops: (Co)Fixpoints are always refolded during iota	Pierre Boutillier	2014-09-18
*	Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.	Hugo Herbelin	2014-09-15
*	Grammar: "avoiding to" isn't proper, either	Jason Gross	2014-08-25
*	Upgrading output tests.	Hugo Herbelin	2014-08-12
*	Fixing output test-suite.	Pierre-Marie Pédrot	2014-07-21
*	cbn understand ! Arguments directive	Pierre Boutillier	2014-06-04