diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-10-06 10:15:26 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-10-06 10:15:26 -0400 |
| commit | 0e84370511179878aa0ebae8bf43810efac194a5 (patch) | |
| tree | bbb81bd1c2dfd38b74df44ae8c236f5353a7a043 /src/elab_ops.sml | |
| parent | 2ed54658340ec7c94084ed21d9a4964b2c6d0afc (diff) | |
Fix a de Bruijn index bug in map fusion
Diffstat (limited to 'src/elab_ops.sml')
| -rw-r--r-- | src/elab_ops.sml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/elab_ops.sml b/src/elab_ops.sml index b5292e9b..f005ab04 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -242,6 +242,9 @@ fun hnormCon env (cAll as (c, loc)) = (case #1 (hnormCon env f') of CMap (dom, _) => let + val inner_f = liftConInCon 0 inner_f + val f = liftConInCon 0 f + val f' = (CApp (inner_f, (CRel 0, loc)), loc) val f' = (CApp (f, f'), loc) val f' = (CAbs ("v", dom, f'), loc) |