X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToWeak.v;h=7fcea20714b5035d64a141a6c54f19f06b8f78bf;hp=ea768560a6fd44829d5e3173bf43d33807377a1b;hb=ee5aaad57d76400e9b8736d4a12d2804f99f329c;hpb=26733c04106397dc8a10396ce688e908e8d0cde7

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index ea76856..7fcea20 100644
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -98,6 +98,7 @@ match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTyp
 | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite)
 | ECase Γ Δ ξ l tc tbranches atypes e alts =>
   fun ite => WECase
+    FIXME
     (strongExprToWeakExpr ftv fcv e ite)
     (@typeToWeakType ftv Γ _ tbranches ite)
     tc