X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=cd4b17bac16f7e46ef08f2531bb9971d4256e977;hp=331744506f87ba066d83a88f3b4de7c690aa318f;hb=26733c04106397dc8a10396ce688e908e8d0cde7;hpb=65a6d16ea7d8a07fe8e162151b76cf40a41d8c31

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 3317445..cd4b17b 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -465,10 +465,10 @@ Definition weakExprToStrongExpr : forall
                                                     τ' _ e >>= fun e' =>
                                                    castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e')
 
-    | WEBrak  ec e tbody                => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
+    | WEBrak  _ ec e tbody              => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' =>
                                              castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e')
 
-    | WEEsc   ec e tbody                => weakTypeToType'' φ tbody ★ >>= fun tbody' =>
+    | WEEsc   _ ec e tbody              => weakTypeToType'' φ tbody ★ >>= fun tbody' =>
                                            match lev with
                                              | nil       => Error "ill-leveled escapification"
                                              | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e