| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Cleaner treatment of parameters in inferCumulativity |  Gaëtan Gilbert | 2018-02-16 |
| * | Fix reduction flags in inferCumulativity | Gaëtan Gilbert | 2018-02-16 |
| * | inferCumulativity: add comment to explain [if not is_arity]. | Gaëtan Gilbert | 2018-02-11 |
| * | Use specialized function for inductive subtyping inference. | Gaëtan Gilbert | 2018-02-11 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |