From e47466025946c307a9c674098eea069b6f3b423c Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Tue, 23 Feb 2021 11:46:30 +0100
Subject: [PATCH] Enforce fraction naming conventions with implicit types

---
 iris/algebra/auth.v         | 4 +++-
 iris/algebra/lib/gset_bij.v | 1 +
 iris/algebra/view.v         | 8 +++++---
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/iris/algebra/auth.v b/iris/algebra/auth.v
index 8556ed2d8..bc52dd8e6 100644
--- a/iris/algebra/auth.v
+++ b/iris/algebra/auth.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export view.
+From iris.algebra Require Export view frac.
 From iris.algebra Require Import proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -86,6 +86,8 @@ Section auth.
   Context {A : ucmra}.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
+  Implicit Types q : frac.
+  Implicit Types dq : dfrac.
 
   Global Instance auth_auth_ne dq : NonExpansive (@auth_auth A dq).
   Proof. rewrite /auth_auth. apply _. Qed.
diff --git a/iris/algebra/lib/gset_bij.v b/iris/algebra/lib/gset_bij.v
index a69296916..c6d29f62f 100644
--- a/iris/algebra/lib/gset_bij.v
+++ b/iris/algebra/lib/gset_bij.v
@@ -114,6 +114,7 @@ Section gset_bij.
   Context `{Countable A, Countable B}.
   Implicit Types (a:A) (b:B).
   Implicit Types (L : gset (A*B)).
+  Implicit Types dq : dfrac.
 
   Global Instance gset_bij_elem_core_id a b : CoreId (gset_bij_elem a b).
   Proof. apply _. Qed.
diff --git a/iris/algebra/view.v b/iris/algebra/view.v
index 6e857ab4f..77c636d2a 100644
--- a/iris/algebra/view.v
+++ b/iris/algebra/view.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Export updates local_updates dfrac agree.
+From iris.algebra Require Export updates local_updates frac dfrac agree.
 From iris.algebra Require Import proofmode_classes big_op.
 From iris.prelude Require Import options.
 
@@ -151,6 +151,8 @@ Section cmra.
   Implicit Types ag : option (dfrac * agree A).
   Implicit Types b : B.
   Implicit Types x y : view rel.
+  Implicit Types q : frac.
+  Implicit Types dq : dfrac.
 
   Global Instance view_auth_ne dq : NonExpansive (@view_auth A B rel dq).
   Proof. solve_proper. Qed.
@@ -390,9 +392,9 @@ Section cmra.
     ●V{dq1} a1 ≼{n} ●V{dq2} a2 ⋅ ◯V b ↔ (dq1 ≼ dq2 ∨ dq1 = dq2) ∧ a1 ≡{n}≡ a2.
   Proof.
     split.
-    - intros [[[[qf agf]|] bf]
+    - intros [[[[dqf agf]|] bf]
         [[?%(discrete_iff _ _) ?]%(inj Some) _]]; simplify_eq/=.
-      + split; [left; apply cmra_included_l|]. apply to_agree_includedN. by exists agf.
+      + split; [left; apply (cmra_included_l dq1)|]. apply to_agree_includedN. by exists agf.
       + split; [right; done|]. by apply (inj to_agree).
     - intros [[[? ->]| ->] ->].
       + rewrite view_auth_dfrac_op -assoc. apply cmra_includedN_l.
-- 
GitLab