diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2010-10-10 14:41:03 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2010-10-10 14:41:03 -0400 |
| commit | 948aa854af8ca5560a1eea5221c4a1f3a6901970 (patch) | |
| tree | 2e1c023171139b80bf24b4ec2b5a85115973e945 /src/elab_util.sml | |
| parent | bfeac162a328dba937a28e747e4fc4006fac500c (diff) | |
Hopeful fix for the Great Unification Bug
Diffstat (limited to 'src/elab_util.sml')
| -rw-r--r-- | src/elab_util.sml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index 33ed599c..d297ccbc 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -118,6 +118,8 @@ fun exists f k = end +val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con) + structure Con = struct datatype binder = @@ -215,7 +217,7 @@ fun mapfoldB {kind = fk, con = fc, bind} = (CProj (c', n), loc)) | CError => S.return2 cAll - | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c + | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c) | CUnif _ => S.return2 cAll | CKAbs (x, c) => |