From 2fabfd72e4944ea3c5c8ab259f402f6f9092f454 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 17 Mar 2021 00:15:37 +0100
Subject: [PATCH] Remove %I which is implied
---
iris/base_logic/upred.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index a369af8d7..d2b54213a 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred {
this way. *)
Local Coercion uPred_holds : uPred >-> Funclass.
Bind Scope bi_scope with uPred.
-Global Arguments uPred_holds {_} _%I _ _ : simpl never.
+Global Arguments uPred_holds {_} _ _ _ : simpl never.
Add Printing Constructor uPred.
Global Instance: Params (@uPred_holds) 3 := {}.
--
GitLab