coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix test suite after change in extraction.	Maxime Dénès	2015-12-15
*	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
*	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
*	Fixing output test-suite: since universe polymorphism, the Print command	Pierre-Marie Pédrot	2014-05-08
*	Fixing #3293 (eta-expansion at "match" printing time was failing	Hugo Herbelin	2014-04-28
*	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot	2014-03-01
*	test-suite: opaque term -> opaque proof	Pierre Boutillier	2014-02-28
*	test-suite: New names for vars but the expected invariant is preserved	Pierre Boutillier	2014-02-28
*	Fix output test-suite 'simpl tactic' -> 'reduction tactics'	Pierre Boutillier	2014-02-28
*	test-suite/output/Notations : evar number change	Pierre Boutillier	2013-12-19
*	Test suite: update output reference.	xclerc	2013-12-02
*	Print logical name rather than path (thus allowing reproducible tests).	xclerc	2013-12-02
*	test-suite fixup	pboutill	2013-11-03
*	Fixing 2 output test-suites.	ppedrot	2013-10-08
*	Fixing some tests from the test-suite.	ppedrot	2013-09-03
*	Fix testsuite so that it works with STM	gareuselesinge	2013-08-08
*	better error message for unexpected renaming (closes #2987)	gareuselesinge	2013-07-29