Commit efc8fb86 authored by Robbert Krebbers's avatar Robbert Krebbers

COFE on gname.

parent b0ed7748
......@@ -16,6 +16,7 @@ Definition gid (Σ : gFunctors) := fin (projT1 Σ).
(** Name of one instance of a particular CMRA in the ghost state. *)
Definition gname := positive.
Canonical Structure gnameC := leibnizC gname.
Definition globalF (Σ : gFunctors) : iFunctor :=
IFunctor (iprodURF (λ i, gmapURF gname (projT2 Σ i))).
......
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