Mercurial > urweb

comparison src/explify.sml @ 1303:c7b9a33c26c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)