From 2c46ae4bd8f9f49554daa31988fd98793cc5601e Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sun, 26 Sep 2021 17:37:52 +0200
Subject: Qualify `Instance` and `Program Instance` as `Global`

This avoids a new warning of Coq 8.14.
---
 lib/Maps.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib/Maps.v')

diff --git a/lib/Maps.v b/lib/Maps.v
index 6bc6e14b..3f43d102 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1604,7 +1604,7 @@ Proof.
   intros. transitivity a0; auto.
 Qed.
 
-Instance Equal_Equivalence : Equivalence Equal := {
+Global Instance Equal_Equivalence : Equivalence Equal := {
   Equivalence_Reflexive := Equal_refl;
   Equivalence_Symmetric := Equal_sym;
   Equivalence_Transitive := Equal_trans
@@ -1633,7 +1633,7 @@ Next Obligation.
   unfold equiv, complement in H0. congruence.
 Qed.
 
-Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
+Global Instance Equal_EqDec : EqDec (T.t A) Equal := Equal_dec.
 
 End EXTENSIONAL_EQUALITY.
 
-- 
cgit