summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-02 14:11:18 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-02 14:11:18 -0500
commit686b727ebba1749f1936cfc39a7b6b1f1f6ebc0a (patch)
tree9a7a5b5d9c691037e497e7f105a998d087ebfe47
parent83f86225d56718fae1f226202efda9d69a5c369f (diff)
Instantiate any Unit unification variables that remain after elaboration
-rw-r--r--src/elaborate.sml5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2839c310..a28d3bf4 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -495,7 +495,10 @@
| _ => false
fun cunifsRemain c =
case c of
- L'.CUnif (_, loc, _, _, ref NONE) => SOME loc
+ L'.CUnif (_, loc, k, _, r as ref NONE) =>
+ (case #1 (hnormKind k) of
+ L'.KUnit => (r := SOME (L'.CUnit, loc); NONE)
+ | _ => SOME loc)
| _ => NONE
val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,