From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sun, 27 Mar 2011 02:26:01 +0000 (-0700)
Subject: improve error message
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=20a9b4934a97e6801d6785ac940f771cb74a8cc1

improve error message
---

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 61993a1..05d059a 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -100,7 +100,8 @@ Section core2proof.
   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
     match coreVarToWeakVar cv with
       | WExprVar wev => match weakTypeToTypeOfKind φ wev ★ with
-                          | Error s => Prelude_error ("Error in top-level xi: " +++ s)
+                          | Error s => Prelude_error ("Error converting weakType of top-level variable "+++
+                                                         toString cv+++": " +++ s)
                           | OK    t => t @@ nil
                         end
       | WTypeVar _   => Prelude_error "top-level xi got a type variable"