From af0efbba5f1c93bcca6d7db7f768a9cadc07bf8b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 9 Oct 2020 18:37:19 +0200
Subject: [PATCH] remove useless parameter, and export public dependencies from
 dfrac

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

diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index 4921bb002..f425c3fd5 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -19,7 +19,8 @@
     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 Import cmra proofmode_classes updates frac.
+From iris.algebra Require Export cmra.
+From iris.algebra Require Import proofmode_classes updates frac.
 From iris Require Import options.
 
 (** An element of dfrac denotes ownership of a fraction, knowledge that a
@@ -158,7 +159,7 @@ Section dfrac.
   Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
   Proof. done. Qed.
 
-  Lemma dfrac_valid_own_discarded q p :
+  Lemma dfrac_valid_own_discarded q :
     ✓ (DfracOwn q ⋅ DfracDiscarded) ↔ (q < 1%Qp)%Qc.
   Proof. done. Qed.
 
-- 
GitLab