From d2dfed5019d07747178a9deb4b31b253e8d17fc2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= <gwenael.delaval@inria.fr>
Date: Tue, 14 Mar 2017 12:14:19 +0100
Subject: [PATCH] Correction of shift/reduce conflict in syntax

Correction: in a contract, the list of objectives cannot be empty.
---
 compiler/heptagon/parsing/hept_parser.mly | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

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 }
 ;