| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-05-13 | Fixes #12233 (wrong printing env in presence of match branches eta-expansion). | Hugo Herbelin | |
| At the same time, we propagate the correct binder relevance in detyping. Note that this would be fixed by enforcing the context of branches in the syntax of "Case". | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |