From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Mon, 14 Mar 2011 09:08:26 +0000 (-0700)
Subject: detect (->) TyCon and substitute FunTy in WeakToCore
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=65a6d16ea7d8a07fe8e162151b76cf40a41d8c31

detect (->) TyCon and substitute FunTy in WeakToCore
---

diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v
index 56c2f48..6b6b61e 100644
--- a/src/HaskWeakTypes.v
+++ b/src/HaskWeakTypes.v
@@ -97,6 +97,7 @@ Definition normalizeWeakType (wt:WeakType) : WeakType := wt.
 Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType :=
   match wt with
     | WTyVarTy  (weakTypeVar v _)     => TyVarTy v
+    | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)
     | WAppTy  t1 t2                   => match (weakTypeToCoreType' t1) with
                                            | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil))
                                            | t1'             => AppTy t1' (weakTypeToCoreType' t2)