From 137c80e9d7cce321f11f100f43ba8b95f880d338 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Jan 2017 23:41:26 +0100
Subject: [PATCH] Remove spurious constRF.

---
 theories/heap_lang/lib/counter.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index deffcca5e..3e68d0297 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -85,10 +85,10 @@ End mono_proof.
 Class ccounterG Σ :=
   CCounterG { ccounter_inG :> inG Σ (authR (optionUR (prodR fracR natR))) }.
 Definition ccounterΣ : gFunctors :=
-  #[GFunctor (constRF (authR (optionUR (prodR fracR natR))))].
+  #[GFunctor (authR (optionUR (prodR fracR natR)))].
 
 Instance subG_ccounterΣ {Σ} : subG ccounterΣ Σ → ccounterG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
 
 Section contrib_spec.
   Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
-- 
GitLab