| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixes #6821 (bug in protecting notation printing from infinite eta-expansion). |  Hugo Herbelin | 2018-02-23 |
| 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 Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |