From 7d0b39f24ab04b276beffa5c42cb996fa85be38e Mon Sep 17 00:00:00 2001 From: Arthur Azevedo de Amorim <arthur.aa@gmail.com> Date: Mon, 14 Sep 2020 14:45:43 -0400 Subject: [PATCH] Fix argument order in comment. --- theories/base_logic/lib/gen_heap.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v index 8504c9296..bfedc069f 100644 --- a/theories/base_logic/lib/gen_heap.v +++ b/theories/base_logic/lib/gen_heap.v @@ -17,7 +17,7 @@ of a location [l], this mechanism allows one to attach "meta" or "ghost" data to locations. This is done as follows: - When one allocates a location, in addition to the point-to connective [l ↦ v], - one also obtains the token [meta_token ⊤ l]. This token is an exclusive + one also obtains the token [meta_token l ⊤]. This token is an exclusive resource that denotes that no meta data has been associated with the namespaces in the mask [⊤] for the location [l]. - Meta data tokens can be split w.r.t. namespace masks, i.e. -- GitLab