Correction of shift/reduce conflict in syntax

Correction: in a contract, the list of objectives cannot be empty.
master
Gwenaël Delaval 7 years ago
parent 0515cf4f80
commit d2dfed5019

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

Loading…
Cancel
Save