Commit fa35bdc6 authored by Hai Dang's avatar Hai Dang
Browse files

Add more TODOs

parent 9d06622c
......@@ -5,6 +5,7 @@ From gpfsl.base_logic Require Import history vprop.
Require Import iris.prelude.options.
(* TODO: lift this monPred of iProp *)
(** Lifts meta into vProp *)
Section meta_vprop_def.
......
......@@ -12,6 +12,7 @@ From gpfsl.lang Require Import notation.
Require Import iris.prelude.options.
(* TODO: move to master *)
Definition ro_ptstoR : cmra := agreeR (leibnizO (time * val * view)).
Class ro_ptstoG Σ := { ro_ptsto_inG :> inG Σ ro_ptstoR; }.
......
Supports Markdown
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