diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index 713c139..140e113 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -206,12 +206,11 @@ node_params:
 
 contract:
   | /* empty */ {None}
-  | CONTRACT loc_vars opt_equs opt_assume enforce opt_with
+  | CONTRACT loc_vars opt_equs opt_assume enforce
       {Some{c_local = $2;
 	    c_eq = $3;
 	    c_assume = $4;
-	    c_enforce = $5;
-	    c_controllables = $6 }}
+	    c_enforce = $5 }}
 ;
 
 opt_equs:
@@ -228,11 +227,6 @@ enforce:
   | ENFORCE exp { $2 }
 ;
 
-opt_with:
-  | /* empty */ { [] }
-  | WITH LPAREN params RPAREN { $3 }
-;
-
 loc_vars:
   | /* empty */    { [] }
   | VAR loc_params { $2 }
diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml
index 6fecee9..b92404a 100644
--- a/compiler/heptagon/parsing/hept_parsetree.ml
+++ b/compiler/heptagon/parsing/hept_parsetree.ml
@@ -115,7 +115,6 @@ and type_desc =
 type contract =
     { c_assume : exp;
       c_enforce : exp;
-      c_controllables : var_dec list;
       c_local : var_dec list;
       c_eq : eq list;
     }