X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=e5c88f8472c3c9002dd34873c3c979115618e28d;hb=ab2e0681a81695cc2380b007f2a3314005ec1c99;hp=d765f0fc035901b7b3d3a1ac52c07f55be873431;hpb=3c72c39a441415f3a9ec78d9f75dcaf72ffab80a;p=coq-hetmet.git

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index d765f0f..e5c88f8 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -19,7 +19,6 @@ Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
-Require Import HaskCoreToWeak.
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
@@ -559,7 +558,7 @@ Definition weakExprToStrongExpr : forall
                                                    weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ te' lev e >>= fun e' =>
                                                      castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e')
 
-    | WECast  e co                      => let (_,t1,t2,_) := co in
+    | WECast  e co                      => let (t1,t2) := weakCoercionTypes co in
                                              weakTypeToType'' φ t1 ★ >>= fun t1' =>
                                                weakTypeToType'' φ t2 ★ >>= fun t2' =>
                                                    weakExprToStrongExpr Γ Δ φ ψ ξ t1' lev e >>= fun e' =>