X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=04e105517e7381b834ddd2ad5594cf7fb4e42db9;hp=1c3ba70fdd8cd7af34577aebb70ab3fbd8b9bdbb;hb=24445b56cb514694c603c342d77cbc8329a4b0aa;hpb=b0303799b3deddd7a19b29be7852f6dafaf04325

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 1c3ba70..04e1055 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -501,6 +501,8 @@ Definition weakExprToStrongExpr : forall
                                                >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e')
                                            end
 
+    | WECSP   _ ec e tbody              => Error "FIXME: CSP not supported beyond HaskWeak stage"
+
     | WENote  n e                       => weakExprToStrongExpr Γ Δ φ ψ ξ τ lev e >>= fun e' => OK (ENote _ _ _ _ n e')
 
     | WELet   v ve  ebody               => weakTypeToTypeOfKind φ v ★  >>= fun tv =>