coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	#3828 is solved.	Hugo Herbelin	2014-12-16
\|
*	Moving #2447 (congruence) to fixed.	Hugo Herbelin	2014-12-16
\|
*	Test for #3654.	Hugo Herbelin	2014-12-16
\|
*	Tests for #3848 and #3854.	Hugo Herbelin	2014-12-15
\|
*	Two fixes in unification (bugs #3782 and #3709)	Matthieu Sozeau	2014-12-12
\| \| \| \| \| \| \| \|	- In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed.
*	New reproduction cases for the test suite.	Xavier Clerc	2014-12-11
\|
*	Commits on evar-evar unification fixed HoTT_coq_106 and improved the	Hugo Herbelin	2014-12-05
\| \| \| \| \|	status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted).
*	Updading test-suite.	Hugo Herbelin	2014-12-03
\|
*	When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if	Hugo Herbelin	2014-12-02
\| \| \| \| \| \| \| \| \| \| \|	possible, which is the "natural" way to orient an equation. At least it matters for matching subterms against patterns, so that it is the pattern variables which are substituted if ever the subterm has itself existential variables, as in: Goal exists x, S x = x. eexists. destruct (S _).
*	Fixing test-suite.	Pierre-Marie Pédrot	2014-12-01
\|
*	Adding test for bug #3417.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test for bug #3485.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test for bug #3487.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test of bug #3682.	Pierre-Marie Pédrot	2014-11-30
\|
*	Bug #3804 is actually closed (thanks to Jason Gross for the notification).	Xavier Clerc	2014-11-25
\|
*	Tweak some test cases.	Xavier Clerc	2014-11-25
\|
*	Adding test for bug #3248.	Pierre-Marie Pédrot	2014-11-24
\|
*	Pass around information on the use of template polymorphism for	Matthieu Sozeau	2014-11-23
\| \| \| \| \| \| \|	inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821).
*	Test for closed #2713 and #2876.	Hugo Herbelin	2014-11-22
\|
*	Adding test for bug #3326.	Pierre-Marie Pédrot	2014-11-21
\|
*	Adding test for bug #3424.	Pierre-Marie Pédrot	2014-11-21
\|
*	Cleaning up closed bugs in test-suite.	Pierre-Marie Pédrot	2014-11-21
\|
*	Test for bug #3788.	Pierre-Marie Pédrot	2014-11-21
\|
*	Add test-suite file for bug #3804.	Matthieu Sozeau	2014-11-21
\|
*	Adding test for bug #3684.	Pierre-Marie Pédrot	2014-11-20
\|
*	Add missing "Fail" to test case for bug #2814.	Xavier Clerc	2014-11-14
\|
*	Reproduction cases for the test suite.	Xavier Clerc	2014-11-14
\|
*	Adding test for bug 3792.	Pierre-Marie Pédrot	2014-11-09
\|
*	Test #3655 was failing due to an anomaly. Now it rather has to fail	Hugo Herbelin	2014-11-08
\| \| \| \|	normally, so failure is now detected by removing the "Fail".
*	Test fixed by PMP's commits from Oct 21.	Hugo Herbelin	2014-11-08
\|
*	Test for #3675 on primitive projections.	Hugo Herbelin	2014-11-07
\|
*	Fixing #3562 ("as" in "destruct" expects either a disjunctive	Hugo Herbelin	2014-11-07
\| \| \| \|	intropattern or a bound ltac variable).
*	Test for #3542 fixed some time ago.	Hugo Herbelin	2014-11-07
\|
*	Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.	Hugo Herbelin	2014-11-06
\|
*	test suite: some reproduction cases for recently-reported bugs.	Xavier Clerc	2014-11-04
\|
*	Test for bug #2149.	Pierre-Marie Pédrot	2014-11-04
\|
*	New bugs revealed fixed: #3408 by (probably) Maxime's commits	Hugo Herbelin	2014-11-03
\| \| \| \| \| \|	on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459.
*	Fix test-suite for #2729.	Maxime Dénès	2014-10-22
\| \| \| \|	Was always failing due to an incorrect use of Ltac's or.
*	More precise test for #3459.	Hugo Herbelin	2014-10-21
\|
*	Fixing a (new) part of bug #2729.	Hugo Herbelin	2014-10-20
\| \| \| \| \| \| \| \| \| \| \|	By moving convert_concl to new proof engine, re-typecheckeing was incidentally introduced. Re-typechecking revealed that vm bug #2729 was still open. Indeed, the vm was still producing an ill-typed term. This commit fixes ill-typedness of the vm in #2729 when reconstructing a "match" in an inductive type whose constructors have let-ins. Another part is still open (see test-suite).
*	Fix test-suite scripts.	Matthieu Sozeau	2014-10-16
\|
*	Bug fixed by Hugo.	Matthieu Sozeau	2014-10-16
\|
*	Adding a timeout to bug #2447.	Pierre-Marie Pédrot	2014-10-15
\|
*	To stay closer to non-primitive projections, only unfold primitive	Matthieu Sozeau	2014-10-15
\| \| \| \| \|	projections in cbv when delta _and_ beta flags are set. Add test-suite file for bug 3700 too.
*	Fix for bug #3618.	Matthieu Sozeau	2014-10-15
\| \| \| \| \|	Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars.
*	Closed bug 3710.	Matthieu Sozeau	2014-10-15
\|
*	Bug 3692 is fixed.	Matthieu Sozeau	2014-10-15
\|
*	Bug 3628 is fixed.	Matthieu Sozeau	2014-10-15
\|
*	Fix test-suite files which failed due to usage of $(admit)$ which	Matthieu Sozeau	2014-10-15
\| \| \| \|	now fails with Error: Already an existential evar of name Main
*	Fix bug 3637.	Matthieu Sozeau	2014-10-15
\|