Commit a412185c authored by Armaël Guéneau's avatar Armaël Guéneau

Document the modification to [app_record_new] wrt recursive records

parent 64771768
......@@ -444,7 +444,11 @@ Hint Resolve affine_record_repr : affine.
(* Axiomatic specification of [new] on a list of fields;
[app_record_new L] is a characteristic formula describing
the allocation of a record. *)
the allocation of a record.
[L] takes the name of the record as an argument: this is useful for records
defined recursively, where fields can point to the record itself. In the
non-recursive case, [L] will be of the form [fun _ => ...]. *)
Definition app_record_new (L:loc -> record_descr) : ~~loc :=
local (fun H Q => (fun r => H \* r ~> record_repr (L r)) ===> Q).
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment