X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=f177e1f144b52704b4687cc476ee1be809476d53;hp=78cd6aedb8f6c8fef9ef3aa50fb32b5aa4e174cc;hb=1f411b48dd607e76a65903e8506d0ae5e7470321;hpb=1758dade15ff584949a9e4bd6b21ce1a58e42ff3

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 78cd6ae..f177e1f 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -119,11 +119,11 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
                         end
     | WELam   (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
     | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
-    | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
+    | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
     | WELet   ev ve e            => weakTypeOfWeakExpr e
     | WELetRec rb e              => weakTypeOfWeakExpr e
     | WENote  n e                => weakTypeOfWeakExpr e
-    | WECast  e (weakCoercion t1 t2 _) => OK t2
+    | WECast  e (weakCoercion _ t1 t2 _) => OK t2
     | WECase  scrutinee tbranches tc type_params alts => OK tbranches
 
     (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)