From 2c1dd0269238edd0076ea0a99e45c8d1d69f55d9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Jan 2021 21:07:36 +0100
Subject: [PATCH] only locally make siProp_holds a coercion

---
 iris/si_logic/siprop.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index 4725abbcc..94778022e 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -6,9 +6,10 @@ From iris.prelude Require Import options.
 define the usual connectives of higher-order logic, and prove that these satisfy
 the usual laws of higher-order logic. *)
 Record siProp := SiProp {
-  siProp_holds :> nat → Prop;
+  siProp_holds : nat → Prop;
   siProp_closed n1 n2 : siProp_holds n1 → n2 ≤ n1 → siProp_holds n2
 }.
+Local Coercion siProp_holds : siProp >-> Funclass.
 Global Arguments siProp_holds : simpl never.
 Add Printing Constructor siProp.
 
-- 
GitLab