This MR introduces several changes intended to make RefinedC more user-friendly.
The first change concern the syntax of constraints in annotations. The following is now allowed:
own l : ty
(previously written l @ &own<ty>
),shr l : ty
(previously written l @ &shr<ty>
),frac β l : ty
(previously written l @ &frac<β, ty>
).The second change is some renaming around singleton types and layouts:
singleton_val
is now called value
,singleton_place
is now called place
,LPtr
is now called void_ptr
and has notation void*
,LVoid
is now called void_layout
.void*
as an identifier.The last change introduces a new Coq scope called printing_sugar
that is only opened at the beginning of proofs in generated proof files. It defines printing notations intended at making the output of the tool closer to the syntax of the front end. In particular it defines the following notations:
own l : ty
, shr l : ty
, frac {β} l : ty
,uninit<ly>
, value<ly, v>
, place<l>
, &own<ty>
, ...