coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
* \|	Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into Jaso...	Matthieu Sozeau	2014-06-26
\|\ \
* \| \|	Fix test-suite files.	Matthieu Sozeau	2014-06-26
* \| \|	Bug #3301 is closed, the projection cannot be defined anymore.	Matthieu Sozeau	2014-06-26
* \| \|	Fix test-suite file for opened bug #1596	Matthieu Sozeau	2014-06-26
* \| \|	Fix test-suite file for bug # 3036, the unification has _never_ succeeded,	Matthieu Sozeau	2014-06-26
* \| \|	Change interface of refresh universes to get a pbty argument instead of	Matthieu Sozeau	2014-06-26
* \| \|	Add an Unset Standard...	Matthieu Sozeau	2014-06-26
\| \| *	Update some bugs about typeclass resolution	Jason Gross	2014-06-24
\| \|/ \|/\|
* \|	Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)	Enrico Tassi	2014-06-23
* \|	Fix for bug 1951, allowing at least fully-applied inductives types to be used	Matthieu Sozeau	2014-06-23
* \|	Fix test-suite script for subst working with let-ins, the following proof was...	Matthieu Sozeau	2014-06-23
* \|	Changed syntax of explicit universes.	Matthieu Sozeau	2014-06-23
* \|	Fix semantics of change p with c to typecheck c at each specific occurrence o...	Matthieu Sozeau	2014-06-23
* \|	Proper handling of the polymorphism flag for Context, fixing HoTT bug #98.	Matthieu Sozeau	2014-06-23
* \|	The uses of the funext axiom forced levels to Set, relaxing its use doesn't.	Matthieu Sozeau	2014-06-23
* \|	The test-suite file couldn't typecheck as it rightly introduces a universe in...	Matthieu Sozeau	2014-06-23
* \|	Fix test-suite script for HoTT coq bug #34	Matthieu Sozeau	2014-06-23
\| *	More test-suite cases	Jason Gross	2014-06-22
\|/
*	- Add an option to refresh only algebraic universes, for e_type_of. The goal	Matthieu Sozeau	2014-06-21
*	Fixed bug 3332.	Matthieu Sozeau	2014-06-20
*	Allow more relaxed conversion between the types of the two terms of a rewrite	Matthieu Sozeau	2014-06-20