coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
\| \| *	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
\| *	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
*	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
*	Not a bug, keep for backwards compatibility	Matthieu Sozeau	2014-06-17
*	Bug closed, now in polymorphic mode, Variables A B : Type give different leve...	Matthieu Sozeau	2014-06-17
*	Explicit universes allow to write liftings explicitely. Implicit lifting woul...	Matthieu Sozeau	2014-06-17
*	Not considering test-suite file #89 as a bug anymore.	Matthieu Sozeau	2014-06-17
*	Continue fix on argument scopes of primitive projections.	Matthieu Sozeau	2014-06-17
*	Fix HoTT bug #84, binding scopes to projections.	Matthieu Sozeau	2014-06-17
*	HoTT coq bug #82 already fixed.	Matthieu Sozeau	2014-06-17
*	Adapt coercion code to work with projections as target classes.	Matthieu Sozeau	2014-06-17
*	- Fix the de Bruijn problem in check_projection for good :)	Matthieu Sozeau	2014-06-17
*	Fix a de Bruijn bug in checking code of projections.	Matthieu Sozeau	2014-06-17
*	Existing Class now works with universe polymorphism. Fixes HoTT bug #063	Matthieu Sozeau	2014-06-17
*	Unification in HoTT_coq_061.v was looping with previous commit (while	Hugo Herbelin	2014-06-16
*	- Add "Show Universes" to print information about universes during a proof.	Matthieu Sozeau	2014-06-16
*	HoTT bug #29 is fixed, using the correct notion of polymorphic product types.	Matthieu Sozeau	2014-06-16
*	Change Ltac constr matching semantics to consider universes when merging two	Matthieu Sozeau	2014-06-15
*	The semantics of Variable x y : T is to have the exact same type T for x and y,	Matthieu Sozeau	2014-06-15
*	Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.	Matthieu Sozeau	2014-06-15
*	- Fix xml plugin treatment of inductives.	Matthieu Sozeau	2014-06-15
*	Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of...	Matthieu Sozeau	2014-06-13
*	HoTT/coq bug #7 is closed, and the definitions can be made to go through usin...	Matthieu Sozeau	2014-06-13
*	Fix bug #3291, stack overflow in rewrite.	Matthieu Sozeau	2014-06-11
*	Fix bug #3289	Matthieu Sozeau	2014-06-11
*	Move bug # 3368 to closed bugs	Matthieu Sozeau	2014-06-11
*	Add many more cases to the test-suite	Jason Gross	2014-06-10
*	Move closed bug 3314	Jason Gross	2014-06-10