From 4e608544ebe87dd991d53ded5267f14f5df93b8b Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 10 Oct 2010 20:33:10 -0400
Subject: :::_ notation; switch to TooDeep error message

---
 src/elab_err.sml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/elab_err.sml')

diff --git a/src/elab_err.sml b/src/elab_err.sml
index f8a16294..7d5e6be8 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -121,6 +121,7 @@ datatype cunify_error =
        | CRecordFailure of con * con * (con * con * con) option
        | TooLifty of ErrorMsg.span * ErrorMsg.span
        | TooUnify of con * con
+       | TooDeep
 
 fun cunifyError env err =
     case err of
@@ -162,6 +163,7 @@ fun cunifyError env err =
         (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable";
          eprefaces' [("Replacement", p_con env c1),
                      ("Body", p_con env c2)])
+      | TooDeep => ErrorMsg.error "Can't reverse-engineer unification variable lifting"
 
 datatype exp_error =
        UnboundExp of ErrorMsg.span * string
-- 
cgit v1.2.3