X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=9607d5f87d6f19359bf2d62898fdd4af2e228325;hp=b6add9448794403c5c9de6c77baff31dfdd1447c;hb=24445b56cb514694c603c342d77cbc8329a4b0aa;hpb=b0303799b3deddd7a19b29be7852f6dafaf04325

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index b6add94..9607d5f 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -59,6 +59,12 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
                                                      (weakExprToCoreExpr e)::
                                                      nil)
                                                    (CoreEVar v)
+  | WECSP   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr e)::
+                                                     nil)
+                                                   (CoreEVar v)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr ve))  (weakExprToCoreExpr e)
   | WECase  vscrut e tbranches tc types alts  =>
                                             CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches)