X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FExtraction.v;h=65f3f2d144b10cc56a49fac75d8ae99492dcf490;hb=1f411b48dd607e76a65903e8506d0ae5e7470321;hp=739124667f56828bcc209053339b2b6259d22688;hpb=1758dade15ff584949a9e4bd6b21ce1a58e42ff3;p=coq-hetmet.git

diff --git a/src/Extraction.v b/src/Extraction.v
index 7391246..65f3f2d 100644
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -78,7 +78,7 @@ Section core2proof.
    * free tyvars in them *)
   Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ :=
     match coreVarToWeakVar cv with
-      | WExprVar wev => match weakTypeToType' φ wev ★ with
+      | WExprVar wev => match weakTypeToType'' φ wev ★ with
                           | Error s => Prelude_error ("Error in top-level xi: " +++ s)
                           | OK    t => t @@ nil
                         end