From 3b0457d4cbb0da39f884b8763b0733e629c891a0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 Feb 2020 08:53:10 +0100
Subject: [PATCH] add another printing hint for normalization
---
tests/proofmode_monpred.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index b76927b8b..268ffa905 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,7 @@
From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants.
Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
+Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
Section tests.
Context {I : biIndex} {PROP : sbi}.
--
GitLab