From da045e6b672bda45dd039fc05c89d44b3facd83b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Jan 2019 15:21:04 +0000
Subject: [PATCH] Rename constructor of `uPred` into `UPred`.

---
 theories/base_logic/upred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 9eb60d424..c7bb90344 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -47,7 +47,7 @@ Local Hint Extern 10 (_ ≤ _) => lia : core.
    connective.
  *)
 
-Record uPred (M : ucmraT) : Type := IProp {
+Record uPred (M : ucmraT) : Type := UPred {
   uPred_holds :> nat → M → Prop;
 
   uPred_mono n1 n2 x1 x2 :
-- 
GitLab