coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into ↵	Matthieu Sozeau	2014-06-26
\|\ \| \| \| \| \| \|	JasonGross-tc
* \|	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
\| \| \| \| \| \| \| \|	the hypotheses in eauto.
* \|	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 ↵	Matthieu Sozeau	2014-06-26
\|\ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	JasonGross-more-test-suite Conflicts: test-suite/bugs/closed/3300.v test-suite/bugs/closed/3373.v
* \| \|	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
\| \| \| \| \| \| \| \|	Every time you use abstract a kitten dies, please stop.
\| *	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
\| \| \| \| \|	there is not the same as in Evd.define. - Fixed bugs #3330 and #3331.
*	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
\| \| \| \|	equation, fix uncaught exception in setoid_rewrite (bug #3336).
*	Fix computation of inductive level in monomorphism + indices-matter mode.	Matthieu Sozeau	2014-06-20
\| \| \| \|	Fixes bug #3346.
*	Fixed some HoTT bugs, provide a proper error message when giving an ill-formed	Matthieu Sozeau	2014-06-20
\| \| \| \|	universe instance.
*	Bug 27 closed now that universe contexts can be refined during the proof,	Matthieu Sozeau	2014-06-20
\| \| \| \|	here instantiating a flexible level with Set.
*	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
\| \| \| \| \| \|	and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup.
*	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 ↵	Matthieu Sozeau	2014-06-17
\| \| \| \|	levels to A and B.
*	Explicit universes allow to write liftings explicitely. Implicit lifting ↵	Matthieu Sozeau	2014-06-17
\| \| \| \| \| \|	would change the theory non-trivially.
*	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 HoTT coq bug #80, implicit arguments with primitive projections were wrongly automatically infered.
*	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
\| \| \| \| \| \| \|	it was failing with Not_found before previous commit). This "fixes" the loop by expanding local defs in "imitate" rather than keeping them explicit. The example is otherwise too large for me to be able to understand where does the loop come from.
*	- Add "Show Universes" to print information about universes during a proof.	Matthieu Sozeau	2014-06-16
\| \| \| \|	- Remove dead code in evarconv.
*	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
\| \| \| \| \|	bindings of the same variable (fixing HoTT bug #52). Document the unification of universes in Ltac/tactics.
*	The semantics of Variable x y : T is to have the exact same type T for x and y,	Matthieu Sozeau	2014-06-15
\| \| \| \|	while Context gives different type to each variable, this test-suite file shows this.
*	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
\| \| \| \|	- Move HoTT bug #30 to closed
*	Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead ↵	Matthieu Sozeau	2014-06-13
\| \| \| \| \| \| \| \|	of an anomaly in case a universe inconsistency occurs when applying a coercion. The statement of the test-suite file cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat to Set.
*	HoTT/coq bug #7 is closed, and the definitions can be made to go through ↵	Matthieu Sozeau	2014-06-13
\| \| \| \| \| \|	using explicit universes. The behavior of Hint Rewrite still differs from Hint Resolve though.
*	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
\| \| \| \| \| \| \| \| \|	I'd add more, but I'm tired and it's late and I should sleep. Maybe I'll pick up at 3279 (working down) another day. Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed, even though it raises an anomaly. So there's no way I can think of to test it. I've left it in the [opened] directory anyway.
*	Move closed bug 3314	Jason Gross	2014-06-10
\|