X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=60b7d0425ddaa8b5a8cb85e47c1eeb07f93e95cf;hp=3c7b69cf91b68c21f28ed6f7b4ebc195bda9c5d3;hb=24445b56cb514694c603c342d77cbc8329a4b0aa;hpb=b0303799b3deddd7a19b29be7852f6dafaf04325

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 3c7b69c..60b7d04 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -35,6 +35,7 @@ Inductive WeakExpr :=
 (* or hetmet_esc identifier                                                *)
 | WEBrak      : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 | WEEsc       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
+| WECSP       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 
 | WECase      : forall (vscrut:WeakExprVar)
                        (scrutinee:WeakExpr)