coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Invalid bug report.	Matthieu Sozeau	2014-06-26
*	Fix bug # 3325 using canonical structure declarations where needed.	Matthieu Sozeau	2014-06-26
*	Add an option to disable typeclass resolution during conversion, which	Matthieu Sozeau	2014-06-26
*	Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into JasonG...	Matthieu Sozeau	2014-06-26
\|\
* \|	Fixed bug with new semantics of change.	Matthieu Sozeau	2014-06-26
* \|	Duplicate	Matthieu Sozeau	2014-06-26
* \|	This has been fixed.	Matthieu Sozeau	2014-06-26
* \|	Properly refresh the local hintdb database in case an external tactic changed	Matthieu Sozeau	2014-06-26
* \|	Fix test-suite file, adding the proper Fail.	Matthieu Sozeau	2014-06-26
* \|	Bug #3329 is closed.	Matthieu Sozeau	2014-06-26
* \|	3392 is now closed thanks to E. Tassi.	Matthieu Sozeau	2014-06-26