From ae905a7d79c7a230374f0ab6d0e8977ffe73275d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Feb 2021 10:05:09 +0100
Subject: [PATCH] silence warnings
---
tests/proofmode_ascii.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index e29a22860..cab53ecec 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -6,6 +6,10 @@ From iris.bi Require Import ascii.
Set Default Proof Using "Type".
+(* Remove this and the [Set Printing Raw Literals.] below once we require Coq
+8.14. *)
+Set Warnings "-unknown-option".
+
Section base_logic_tests.
Context {M : ucmra}.
Implicit Types P Q R : uPred M.
--
GitLab