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.
---
 driver/Compiler.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'driver')

diff --git a/driver/Compiler.v b/driver/Compiler.v
index 75247f71..b00d067e 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -209,7 +209,7 @@ Proof.
   intros. unfold match_if, partial_if in *. destruct (flag tt). auto. congruence.
 Qed.
 
-Instance TransfIfLink {A: Type} {LA: Linker A}
+Global Instance TransfIfLink {A: Type} {LA: Linker A}
                       (flag: unit -> bool) (transf: A -> A -> Prop) (TL: TransfLink transf)
                       : TransfLink (match_if flag transf).
 Proof.
-- 
cgit