X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=dbeb3ccec21ea55152b6015ccd2fa9d0f529cd70;hp=61993a1515802b1d9f14e812de3ad19a864f4450;hb=e536cc4194f350ed6de5d465bcf53fda650b3d12;hpb=992203bb4a221ea2f415c0d14bb34d35af2ee637

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 61993a1..dbeb3cc 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -40,7 +40,7 @@ Require Import HaskProofCategory.
 (*
 Require Import HaskStrongCategory.
 *)
-Require Import ReificationsEquivalentToGeneralizedArrows.
+Require Import ReificationsIsomorphicToGeneralizedArrows.
 
 Open Scope string_scope.
 Extraction Language Haskell.
@@ -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"