From 2f5ef3ed69041e85e5ad336d7a22cf7e3ec03949 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 May 2020 09:18:52 +0200
Subject: [PATCH] fix proofmode_ascii test on latest Coq
---
tests/proofmode_ascii.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index 877098dc6..4be27f36e 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
From iris.bi Require Import ascii.
Set Default Proof Using "Type".
+Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
Section base_logic_tests.
Context {M : ucmraT}.
--
GitLab