Commit 5af652a4 authored by Sylvain Dailler's avatar Sylvain Dailler

parser: remove name and parse requires/assert names as ident_nq

parent 5214043f
......@@ -1082,11 +1082,11 @@ single_expr_:
{ Ematch ($2, [], $4) }
| GHOST single_expr
{ Eghost $2 }
| assertion_kind option(name) LEFTBRC term RIGHTBRC
| assertion_kind option(ident_nq) LEFTBRC term RIGHTBRC
{ match $2 with
| None -> Eassert ($1, $4)
| Some name ->
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name)) in
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name.id_str)) in
let t = { $4 with term_desc = Tattr (attr, $4) } in
Eassert ($1, t) }
| attr single_expr %prec prec_attr
......@@ -1187,16 +1187,12 @@ spec:
| (* epsilon *) %prec prec_no_spec { empty_spec }
| single_spec spec { spec_union $1 $2 }
name:
| LIDENT { $1 }
| UIDENT { $1 }
single_spec:
| REQUIRES option(name) LEFTBRC term RIGHTBRC
| REQUIRES option(ident_nq) LEFTBRC term RIGHTBRC
{ match $2 with
| None -> { empty_spec with sp_pre = [$4] }
| Some name ->
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name)) in
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name.id_str)) in
let t = { $4 with term_desc = Tattr (attr, $4) } in
{ empty_spec with sp_pre = [t] } }
| ENSURES LEFTBRC ensures RIGHTBRC
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment