diff --git a/iris/algebra/dra.v b/iris/algebra/dra.v
index 01ed39ecf09abe6756764e625e98536b0a813f65..d8355e2ed23036f8cb38d1cd3037effd20c8d3e2 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.