From d856d6ea4efaba98bbb55a0ef5070703f7fcbfc9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Nov 2021 15:20:19 -0500
Subject: [PATCH] silence a warning we cannot fix any time soon

---
 _CoqProject | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/_CoqProject b/_CoqProject
index 78d8e4df..d6dd2d82 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,8 @@
 -Q theories stdpp
 # 'Global Hint Rewrite' not supported before Coq 8.14.
 -arg -w -arg -deprecated-hint-rewrite-without-locality
+# Fixing this one requires Coq 8.15.
+-arg -w -arg -deprecated-typeclasses-transparency-without-locality
 
 theories/options.v
 theories/base.v
-- 
GitLab