coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Add a test-suite file ensuring coinductives with primitive projections	Matthieu Sozeau	2015-03-03
\| \| \| \| \|	do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching.
*	Fix test-suite file, this is currently a wontfix, but keep the	Matthieu Sozeau	2015-03-03
\| \| \| \|	test-suite file for when we move to a better implementation.
*	Fix bug #4103: forgot to allow unfolding projections of cofixpoints like	Matthieu Sozeau	2015-03-03
\| \| \| \|	cases, in some cases.
*	Fix bug #4101, noccur_evar's expand_projection can legitimately fail	Matthieu Sozeau	2015-03-03
\| \| \| \|	when called from w_unify, so we protect it.
*	Fix bug #4097.	Matthieu Sozeau	2015-03-02
\|
*	Adding a test for bug #3612.	Pierre-Marie Pédrot	2015-02-27
\|
*	Test for bug #3249.	Pierre-Marie Pédrot	2015-02-27
\|
*	Fix test for #3467, I had moved it in a dumb way.	Maxime Dénès	2015-02-27
\|
*	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
\| \| \| \| \| \| \| \| \|	is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
*	Fixing first part of bug #3210 (inference of pattern-matching return	Hugo Herbelin	2015-02-27
\| \| \| \|	clause in the presence of let-ins in the arity of inductive type).
*	Fix test for #3848, still open.	Maxime Dénès	2015-02-27
\|
*	Moving test for #3467 to closed after PMP's fix.	Maxime Dénès	2015-02-27
\|
*	Fix test-suite files for bugs #2456 and #3593, still open.	Maxime Dénès	2015-02-27
\|
*	Add test-suite file for #3649.	Maxime Dénès	2015-02-27
\|
*	Moving tests for #2456 and #3593 to "opened" until they're fixed.	Maxime Dénès	2015-02-27
\|
*	Made test for #3392 rely less on unification.	Maxime Dénès	2015-02-27
\|
*	Moving test of #3848 to "opened".	Maxime Dénès	2015-02-27
\|
*	Test for #2602, which seems now fixed.	Maxime Dénès	2015-02-26
\|
*	Test for bug #3298.	Pierre-Marie Pédrot	2015-02-26
\|
*	Fixing complexity tests for #4076.	Maxime Dénès	2015-02-26
\|
*	Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."	Maxime Dénès	2015-02-26
\| \| \| \| \| \| \| \| \|	This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was breaking compatibility because one could no longer use names of foralls in the goal without introducting them. Probably not good style, but it did break many existing developments including CompCert. Closes #4093 but reopens #4035.
*	Moving test for bug #3681 as closed.	Pierre-Marie Pédrot	2015-02-26
\|
*	Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).	Hugo Herbelin	2015-02-25
\|
*	Univs: Fix Check calling the kernel to retype in the wrong environment.	Matthieu Sozeau	2015-02-24
\| \| \| \|	Fixes bug #4089.
*	Compensating 6fd763431 on postponing subtyping evar-evar problems.	Hugo Herbelin	2015-02-23
\| \| \| \| \| \| \|	Pushing pending problems had the side-effect of later solving them in the opposite order as they arrived, resulting on different complexity (see e.g. #4076). We now take care of pushing them in reverse order so that they are treated in the same order.
*	Fix some typos in comments.	Guillaume Melquiond	2015-02-23
\|
*	Test for #3953 (subst in evar instances).	Hugo Herbelin	2015-02-23
\|
*	Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.	Hugo Herbelin	2015-02-23
\| \| \| \| \| \| \| \| \| \| \| \|	This was broken by the attempt to use the same algorithm for rewriting closed subterms than for rewriting subterms with evars: the algorithm to find subterms (w_unify_to_subterm) did not go through evars. But what to do when looking say, for a pattern "S ?n" in a goal "S ?x[a:=S ?y]"? Should we unify ?x[a:=S ?y] with ?n or consider ?x as rigid and look in the instance? If we adopt the first approach, then, what to do when looking for "S ?n" in a goal "?x[a:=S ?y]"? Failing? Looking in the instance? Is it normal that an evar behaves as a rigid constant when it cannot be unified with the pattern?
*	Fixing occur-check which was too strong in unification.ml.	Hugo Herbelin	2015-02-23
\|
*	Fixing test #2830.	Pierre-Marie Pédrot	2015-02-23
\|
*	Fixing test for bug #3071.	Pierre-Marie Pédrot	2015-02-23
\|
*	Moving test for bug #3071.	Pierre-Marie Pédrot	2015-02-21
\|
*	Test for bug #4078.	Pierre-Marie Pédrot	2015-02-21
\|
*	A fix for #3993 (not fully applied term to destruct when eqn is given).	Hugo Herbelin	2015-02-20
\|
*	Fix bug #3938	Matthieu Sozeau	2015-02-18
\|
*	Remove some dead code and add test-suite file.	Matthieu Sozeau	2015-02-16
\|
*	Add test-suite file for #3960.	Matthieu Sozeau	2015-02-16
\|
*	Test for bug #3922.	Pierre-Marie Pédrot	2015-02-16
\|
*	Fixing bug #4035 (support for dependent destruction within ltac code).	Hugo Herbelin	2015-02-16
\|
*	Test for #2946 (trunk bug with let's in unification).	Hugo Herbelin	2015-02-16
\|
*	Fixing test for bug #3944.	Pierre-Marie Pédrot	2015-02-16
\|
*	Test for bug #3944.	Pierre-Marie Pédrot	2015-02-16
\|
*	Undo: back to 8.4 semantics (Close #3514)	Enrico Tassi	2015-02-15
\| \| \| \|	Only tactics are taken into account.
*	Fix test-suite file. Check that definitions do work when sharing is	Matthieu Sozeau	2015-02-15
\| \| \| \|	disabled in the kernel.
*	Test for bug #3490.	Pierre-Marie Pédrot	2015-02-15
\|
*	Test for bug #3916.	Pierre-Marie Pédrot	2015-02-15
\|
*	Fixing test-suite.	Pierre-Marie Pédrot	2015-02-15
\|
*	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
\| \| \| \|	Of course such proofs cannot be processed asynchronously
*	Test for bug #4016.	Pierre-Marie Pédrot	2015-02-14
\|
*	Univs: fix bug #3755. We were missing refreshements of universes in	Matthieu Sozeau	2015-02-14
\| \| \| \|	unifications ?X ~= ?Y foo not catched by solve_evar_evar.