Commit 137c80e9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove spurious constRF.

parent adac2c8b
...@@ -85,10 +85,10 @@ End mono_proof. ...@@ -85,10 +85,10 @@ End mono_proof.
Class ccounterG Σ := Class ccounterG Σ :=
CCounterG { ccounter_inG :> inG Σ (authR (optionUR (prodR fracR natR))) }. CCounterG { ccounter_inG :> inG Σ (authR (optionUR (prodR fracR natR))) }.
Definition ccounterΣ : gFunctors := Definition ccounterΣ : gFunctors :=
#[GFunctor (constRF (authR (optionUR (prodR fracR natR))))]. #[GFunctor (authR (optionUR (prodR fracR natR)))].
Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ ccounterG Σ. Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ ccounterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. Proof. solve_inG. Qed.
Section contrib_spec. Section contrib_spec.
Context `{!heapG Σ, !ccounterG Σ} (N : namespace). Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
......
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