From 25469570c7ca130b1f9c6607edb53e90417e8a1f Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 15 Nov 2021 15:19:37 -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 c505f549b..3748f986d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -15,6 +15,8 @@ # Cannot use non-canonical projections as it causes massive unification failures # (https://github.com/coq/coq/issues/6294). -arg -w -arg -redundant-canonical-projection +# Fixing this one requires Coq 8.15. +-arg -w -arg -deprecated-typeclasses-transparency-without-locality iris/prelude/options.v iris/prelude/prelude.v -- GitLab