coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a test-suite for second-order matching order and indexes.	Pierre-Marie Pédrot	2014-09-02
*	Another fix than 19a7a5789c to avoid descend_in_conjunction to use	Hugo Herbelin	2014-09-02
*	An apply test.	Hugo Herbelin	2014-09-02
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Not using a "cut" in descend_in_conjunctions induced more success. We	Hugo Herbelin	2014-08-29
*	Add test-suite file. Compute the name for the record binder in the	Matthieu Sozeau	2014-08-29
*	Fix bugs #3484 and #3546.	Matthieu Sozeau	2014-08-28
*	There are some occurs-check cases that can be handled by imitation (using pru...	Matthieu Sozeau	2014-08-28
*	Fixing an unnatural selection of subterms larger than expected in the	Hugo Herbelin	2014-08-28
*	Adding test-suite for bug #3212.	Pierre-Marie Pédrot	2014-08-28
*	Add a regression test for 3427	Jason Gross	2014-08-26
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
*	Fix computation of dangling constraints at the end of a proof (bug #3531).	Matthieu Sozeau	2014-08-25
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	instanciation is French, instantiation is English	Jason Gross	2014-08-25
*	Grammar: "avoiding to" isn't proper, either	Jason Gross	2014-08-25
*	Fixing a bug introduced in the extension of 'apply in' + simplifying code.	Hugo Herbelin	2014-08-25
*	Fix test-suite file.	Matthieu Sozeau	2014-08-23
*	Fixing unification of subterms identified by patterns.	Hugo Herbelin	2014-08-18
*	A reorganization of the "assert" tactics (hopefully uniform naming	Hugo Herbelin	2014-08-18
*	Fix test-suite file.	Matthieu Sozeau	2014-08-18
*	Fix test-suite files.	Matthieu Sozeau	2014-08-18
*	Fix test-suite file.	Matthieu Sozeau	2014-08-18
*	Fixing too restrictive detection of resolution of evars in "apply in"	Hugo Herbelin	2014-08-16
*	Restrict eta-conversion to inductive records, fixing bug #3310.	Matthieu Sozeau	2014-08-14
*	Fix test-suite files according to new parsing rule for application of primitive	Matthieu Sozeau	2014-08-13
*	Upgrading output tests.	Hugo Herbelin	2014-08-12
*	Bug #3469: fixing unterminated comment.	Hugo Herbelin	2014-08-12
*	In bug #2406, renouncing to test failure of parsing error.	Hugo Herbelin	2014-08-12
*	Fix unification which was failing when unifying a primitive projection against	Matthieu Sozeau	2014-08-09
*	Fix evarconv not applying eta when it used to. Fixes bug#3319.	Matthieu Sozeau	2014-08-08
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	Fixing #3483 (graceful failing with notations to non-constructors in "match").	Hugo Herbelin	2014-08-03
*	Finish fixes on notations and primitive projections, add test-suite files for...	Matthieu Sozeau	2014-07-31
*	Add test-suite file for bug #3439.	Matthieu Sozeau	2014-07-30
*	Add test-suite file for bug 3454.	Matthieu Sozeau	2014-07-29
*	Add test-suite file for bug #3453	Matthieu Sozeau	2014-07-29
*	fixup fakeide test-suite	Pierre Boutillier	2014-07-24
*	Add test-suite file for guard condition on cofixpoints.	Maxime Dénès	2014-07-22
*	Fixing output test-suite.	Pierre-Marie Pédrot	2014-07-21
*	Adding a test-suite for bug #3422.	Pierre-Marie Pédrot	2014-07-21
*	Adding a test-suite for bug #3416.	Pierre-Marie Pédrot	2014-07-16
*	Fix Funind test-suite file after patch by Pierre.	Matthieu Sozeau	2014-07-11
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...	Matthieu Sozeau	2014-07-03
*	Indeed simpl never is really honored now.	Matthieu Sozeau	2014-07-02
*	Tests for bugs #2834 and #2994.	Hugo Herbelin	2014-06-30
*	Completing test for bug report #2830	Hugo Herbelin	2014-06-30
*	Synchronized names from the "as" clause with the skeleton of the	Hugo Herbelin	2014-06-30
*	Quickly fixing bug #2996: typing functions now check when referring to	Hugo Herbelin	2014-06-28