From e4980084bef9df2439b9adab8545e0219c83e640 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Oct 2020 16:49:17 +0200
Subject: [PATCH] generalize dfrac IsOp instance

---
 theories/algebra/dfrac.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index 9c7e4e32f..4921bb002 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -19,7 +19,7 @@
     that no one can own 1. And, since discarding is an irreversible operation,
     it also implies that no one can own 1 in the future *)
 From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Export cmra proofmode_classes updates.
+From iris.algebra Require Import cmra proofmode_classes updates frac.
 From iris Require Import options.
 
 (** An element of dfrac denotes ownership of a fraction, knowledge that a
@@ -162,8 +162,10 @@ Section dfrac.
     ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1%Qp)%Qc.
   Proof. done. Qed.
 
-  Global Instance is_op_frac q : IsOp' (DfracOwn q) (DfracOwn (q/2)) (DfracOwn (q/2)).
-  Proof. by rewrite /IsOp' /IsOp dfrac_op_own Qp_div_2. Qed.
+  Global Instance dfrac_is_op q q1 q2 :
+    IsOp q q1 q2 →
+    IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
+  Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
 
   (** Discarding a fraction is a frame preserving update. *)
   Lemma dfrac_discard_update q : DfracOwn q ~~> DfracDiscarded.
-- 
GitLab