From 44039dce04269c34baa29b288bb13b6af1ecdd29 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 25 May 2021 13:24:11 +0200
Subject: [PATCH] make some DRA instances Local

---
 iris/algebra/dra.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index 01ed39ecf..d8355e2ed 100644
--- a/iris/algebra/dra.v
+++ b/iris/algebra/dra.v
@@ -44,7 +44,8 @@ Global Arguments dra_op : simpl never.
 Global Arguments dra_valid : simpl never.
 Global Arguments dra_mixin : simpl never.
 Add Printing Constructor draT.
-Global Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
+(* FIXME: Should some of these be [Global]? *)
+Local Existing Instances dra_equiv dra_pcore dra_disjoint dra_op dra_valid.
 
 (** Lifting properties from the mixin *)
 Section dra_mixin.
-- 
GitLab