diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly
index 168979f..46ea168 100644
--- a/compiler/heptagon/parsing/hept_parser.mly
+++ b/compiler/heptagon/parsing/hept_parser.mly
@@ -263,7 +263,7 @@ node_params:
 
 contract:
   | /* empty */ {None}
-  | CONTRACT b=opt_block a=opt_assume ol=objectives w=opt_with
+  | CONTRACT b=opt_block a=opt_assume ol=nonempty_list(objective) w=opt_with
       { Some{ c_block = b;
               c_assume = a;
               c_objectives = ol;
@@ -282,11 +282,6 @@ opt_assume:
   | ASSUME exp { $2 }
 ;
 
-objectives:
-  | /* empty */ { [] }
-  | o=objective ol=objectives { o :: ol }
-;
-
 objective:
   | objective_kind exp    { mk_objective $1 $2 }
 ;