update baked in CoqPass.hs

[coq-hetmet.git] / src / HaskWeakToCore.v

diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v
index 290d634..8ceb0b7 100644 (file)
--- a/src/HaskWeakToCore.v
+++ b/src/HaskWeakToCore.v
@@ -8,7 +8,8 @@ Require Import General.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
@@ -71,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))::