coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Add fixed test-suite file for 3373.	Matthieu Sozeau	2014-06-20
*	Fix computation of inductive level in monomorphism + indices-matter mode.	Matthieu Sozeau	2014-06-20
*	Fixed some HoTT bugs, provide a proper error message when giving an ill-formed	Matthieu Sozeau	2014-06-20
*	Bug 27 closed now that universe contexts can be refined during the proof,	Matthieu Sozeau	2014-06-20
*	HoTT coq bug #62 fixed.	Matthieu Sozeau	2014-06-19
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Fix a destArity that does not exactly match isArity in presence of let-ins.	Matthieu Sozeau	2014-06-17
*	Reinstate eta for records in evarconv, fixing two HoTT coq bugs.	Matthieu Sozeau	2014-06-17