From be24297e3f28d057c39ceff6c1ec4a9942c08054 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 22 Aug 2016 22:47:04 +0200
Subject: [PATCH] Do not use [ucmraT]s as argument of inG.

Since [inG] ranges over [cmraT]s, using an [ucmraT]s results in
[ucmra_cmraR] coercions that slow down type checking.

This commit improves the compilation time of thread_local.v by 40%.
---
 program_logic/iris.v         | 8 ++++----
 program_logic/thread_local.v | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/program_logic/iris.v b/program_logic/iris.v
index b32b16f07..8269a5982 100644
--- a/program_logic/iris.v
+++ b/program_logic/iris.v
@@ -3,10 +3,10 @@ From iris.prelude Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
 
 Class irisPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
-  state_inG :> inG Σ (authUR (optionUR (exclR (stateC Λ))));
-  invariant_inG :> inG Σ (authUR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
-  enabled_inG :> inG Σ coPset_disjUR;
-  disabled_inG :> inG Σ (gset_disjUR positive);
+  state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
+  invariant_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+  enabled_inG :> inG Σ coPset_disjR;
+  disabled_inG :> inG Σ (gset_disjR positive);
 }.
 
 Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index f37c90474..b7619d4e9 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -5,7 +5,7 @@ Import uPred.
 Definition thread_id := gname.
 
 Class thread_localG Σ :=
-  tl_inG :> inG Σ (prodUR coPset_disjUR (gset_disjUR positive)).
+  tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
 
 Definition tlN : namespace := nroot .@ "tl".
 
@@ -47,7 +47,7 @@ Section proofs.
     â–· P ={E}=> tl_inv tid N P.
   Proof.
     iIntros "HP".
-    iVs (own_empty tid) as "Hempty".
+    iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
     iVs (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
       apply (gset_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)).
-- 
GitLab