X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToCore.v;h=8ceb0b73265c947b1505dfdc1fd50f4263986ee6;hp=f5a3f1a021b08d8ff6960513862d3be96d31d51e;hb=a9a60dc234f76a4740b32c0f62aa0fe3a89fea83;hpb=1c1cdb9014f409248ca96b677503719916b2b477

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index f5a3f1a..8ceb0b7 100644
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -72,7 +72,7 @@ Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar :=
   | WENote  n e                          => CoreENote n  (weakExprToCoreExpr e )
   | WELam   (weakExprVar ev _  ) e       => CoreELam  ev (weakExprToCoreExpr e )
   | WETyLam (weakTypeVar tv _  ) e       => CoreELam  tv (weakExprToCoreExpr e )
-  | WECoLam (weakCoerVar cv _ _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
+  | WECoLam (weakCoerVar cv   _ _) e     => CoreELam  cv (weakExprToCoreExpr e )
   | WECast  e co                         => CoreECast    (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co)
   | WEBrak  v (weakTypeVar ec _) e t     => fold_left CoreEApp
                                                    ((CoreEType (TyVarTy ec))::