| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-19 | Fixing wrong notation level in #3295. | Hugo Herbelin | |
| 2014-12-16 | #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-15 | Tests for #3848 and #3854. | Hugo Herbelin | |
| 2014-12-12 | Two fixes in unification (bugs #3782 and #3709) | Matthieu Sozeau | |
| - 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. | |||
| 2014-12-11 | New reproduction cases for the test suite. | Xavier Clerc | |
| 2014-12-05 | Commits on evar-evar unification fixed HoTT_coq_106 and improved the | Hugo Herbelin | |
| status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted). | |||
| 2014-12-03 | Updading test-suite. | Hugo Herbelin | |
| 2014-12-02 | When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if | Hugo Herbelin | |
| 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 _). | |||
| 2014-12-01 | Fixing test-suite. | Pierre-Marie Pédrot | |
| 2014-11-30 | 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-25 | 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-24 | Adding test for bug #3248. | Pierre-Marie Pédrot | |
| 2014-11-23 | Pass around information on the use of template polymorphism for | Matthieu Sozeau | |
| 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). | |||
| 2014-11-22 | Test for closed #2713 and #2876. | Hugo Herbelin | |
| 2014-11-21 | 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-20 | Adding test for bug #3684. | Pierre-Marie Pédrot | |
| 2014-11-14 | Add missing "Fail" to test case for bug #2814. | Xavier Clerc | |
| 2014-11-14 | Reproduction cases for the test suite. | Xavier Clerc | |
| 2014-11-09 | Adding test for bug 3792. | Pierre-Marie Pédrot | |
| 2014-11-08 | Test #3655 was failing due to an anomaly. Now it rather has to fail | Hugo Herbelin | |
| normally, so failure is now detected by removing the "Fail". | |||
| 2014-11-08 | Test fixed by PMP's commits from Oct 21. | Hugo Herbelin | |
| 2014-11-07 | Test for #3675 on primitive projections. | Hugo Herbelin | |
| 2014-11-07 | Fixing #3562 ("as" in "destruct" expects either a disjunctive | Hugo Herbelin | |
| intropattern or a bound ltac variable). | |||
| 2014-11-07 | Test for #3542 fixed some time ago. | Hugo Herbelin | |
| 2014-11-06 | Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels. | Hugo Herbelin | |
| 2014-11-04 | test suite: some reproduction cases for recently-reported bugs. | Xavier Clerc | |
| 2014-11-04 | Test for bug #2149. | Pierre-Marie Pédrot | |
| 2014-11-03 | New bugs revealed fixed: #3408 by (probably) Maxime's commits | Hugo Herbelin | |
| on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459. | |||
| 2014-10-22 | Fix test-suite for #2729. | Maxime Dénès | |
| Was always failing due to an incorrect use of Ltac's or. | |||
| 2014-10-21 | More precise test for #3459. | Hugo Herbelin | |
| 2014-10-20 | Fixing a (new) part of bug #2729. | Hugo Herbelin | |
| 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). | |||
| 2014-10-16 | Fix test-suite scripts. | Matthieu Sozeau | |
| 2014-10-16 | Bug fixed by Hugo. | Matthieu Sozeau | |
| 2014-10-15 | 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 | |
| projections in cbv when delta _and_ beta flags are set. Add test-suite file for bug 3700 too. | |||
| 2014-10-15 | Fix for bug #3618. | Matthieu Sozeau | |
| Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars. | |||
| 2014-10-15 | 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 | |
| now fails with Error: Already an existential evar of name Main | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |