X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;fp=src%2FHaskWeakToCore.v;h=24eedc6bbcd9bb2f3c36ccf6b0b8b37390100151;hp=cfaf65e21f9cc4652e1004241069a37e9c50d873;hb=26733c04106397dc8a10396ce688e908e8d0cde7;hpb=65a6d16ea7d8a07fe8e162151b76cf40a41d8c31

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index cfaf65e..24eedc6 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -53,10 +53,18 @@ Section HaskWeakToCore.
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr f e )
   | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr f e )
   | WECast  e co                         => CoreECast    (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co)
-  | WEBrak  (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_brak_var)
-                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
-  | WEEsc   (weakTypeVar ec _) e t       => CoreEApp  (CoreEApp (CoreEVar hetmet_esc_var)
-                                                           (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t))
+  | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr f e)::
+                                                     nil)
+                                                   (CoreEVar v)
+  | WEEsc   v (weakTypeVar ec _) e t     => fold_left CoreEApp
+                                                   ((CoreEType (TyVarTy ec))::
+                                                     (CoreEType (weakTypeToCoreType t))::
+                                                     (weakExprToCoreExpr f e)::
+                                                     nil)
+                                                   (CoreEVar v)
   | WELet   (weakExprVar v _) ve e       => mkCoreLet      (CoreNonRec v (weakExprToCoreExpr f ve))  (weakExprToCoreExpr f e)
   | WECase  e tbranches tc types alts    => let (v,f') := next _ _ f tt  in
                                             CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches)