add support for CSP in HaskCore+HaskWeak

[coq-hetmet.git] / src / HaskWeak.v

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 3c7b69c..60b7d04 100644 (file)
--- 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)