Mercurial > urweb

diff src/elab_util.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 9e0fa4f6ac93
line wrap: on
line diff
--- a/src/elab_util.sml	Sun Oct 10 13:07:38 2010 -0400
+++ b/src/elab_util.sml	Sun Oct 10 14:41:03 2010 -0400
@@ -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 @@
 
 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 @@
                            (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) =>