Mercurial > urweb
comparison src/explify.sml @ 1303:c7b9a33c26c8
Hopeful fix for the Great Unification Bug
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 10 Oct 2010 14:41:03 -0400 |
parents | d008c4c43a0a |
children | 6c00d8af6239 |
comparison
equal
deleted
inserted
replaced
1302:d008c4c43a0a | 1303:c7b9a33c26c8 |
---|---|
74 | 74 |
75 | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc) | 75 | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc) |
76 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) | 76 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) |
77 | 77 |
78 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) | 78 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) |
79 | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c | 79 | L.CUnif (nl, _, _, _, ref (SOME c)) => explifyCon (ElabEnv.mliftConInCon nl c) |
80 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) | 80 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) |
81 | 81 |
82 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc) | 82 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc) |
83 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc) | 83 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc) |
84 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc) | 84 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc) |