| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-23 | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion). | Hugo Herbelin | |
| More precisely when matching "f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z" do not allow expansion of f since otherwise, we recursively have to match "f t" with the same pattern. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |