| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-11-15 | Intern application arguments in left-to-right order | Gaëtan Gilbert | |
| This makes it so that we have an application `h a b` with both `a` and `b` unbound, `a` is the one that is reported (parent commit with my current compiler setup reports `b` first, and the code does not define which it should be). Ideally we would report both but that requires more code. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |