Commit 64aa3577 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix camera `cntCmra` to use `ZO`.

`LeibnizO` should only be used for `Canonical Structure` declarations.
parent d768c93d
......@@ -9,7 +9,7 @@ From Require Import fractional.
From iris.heap_lang.lib Require Import par.
Definition cntCmra : cmraT := (prodR fracR (agreeR (leibnizO Z))).
Definition cntCmra : cmraT := prodR fracR (agreeR ZO).
Class cntG Σ := CntG { CntG_inG :> inG Σ cntCmra }.
Definition cntΣ : gFunctors := #[GFunctor cntCmra ].
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