diff options
| author | Hugo Herbelin | 2015-10-17 17:26:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-18 20:11:14 +0200 |
| commit | 8748947349a206a502e43cfe70e3397ee457c4f7 (patch) | |
| tree | e1fb17ec7aee812b7ca462c8c644d0155ae88d44 /kernel | |
| parent | 23545b802a14b2fad10f4382604c71f55b7d6d0e (diff) | |
Fixing #4198 (continued): not matching within the inner lambdas/let-ins
of the return clause and of the branches (what assumed that the
implementation preserves the invariant that the return predicate and
the branches are in canonical [fun Δ => t] form, with Δ possibly
containing let-ins).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions