diff options
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) |