| Commit message (Expand) | Author | Age |
|---|
| * | Fix test-suite file, this is currently a wontfix, but keep the |  Matthieu Sozeau | 2015-03-03 |
| * | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | Matthieu Sozeau | 2015-03-03 |
| * | Fix bug #4101, noccur_evar's expand_projection can legitimately fail | Matthieu Sozeau | 2015-03-03 |
| * | 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 |
| * | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin | 2015-02-27 |
| * | 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 |
| * | 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 |
| * | Compensating 6fd763431 on postponing subtyping evar-evar problems. | Hugo Herbelin | 2015-02-23 |
| * | 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 |
| * | 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 |
| * | Fix test-suite file. Check that definitions do work when sharing is | Matthieu Sozeau | 2015-02-15 |
| * | 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 |
| * | 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 |
| * | Univs: When computing the level of an inductive including indices, lets | Matthieu Sozeau | 2015-02-14 |
Matthieu Sozeau
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Guillaume Melquiond
Matthieu Sozeau
Enrico Tassi