| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins). |  Hugo Herbelin | 2017-01-22 |
| * | Fixing a vm_compute bug in the presence of let-ins among the | Hugo Herbelin | 2015-11-22 |
| * | Fixing a bug of adjust_subst_to_rel_context. | Hugo Herbelin | 2015-11-22 |
| * | Fixing kernel bug in typing match with let-ins in the arity. | Hugo Herbelin | 2015-11-22 |
| * | Fixing first part of bug #3210 (inference of pattern-matching return | Hugo Herbelin | 2015-02-27 |
| * | Fixing a bug in the presence of let-in in inductive arity. | Hugo Herbelin | 2014-10-20 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |