From 51b61ebb300438f21fc49a65955c67df879861cd Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 11 Dec 2017 16:55:20 +0100
Subject: [PATCH] Params instance for bupd.

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

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index c83392c9e..195a6040b 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -318,6 +318,7 @@ Definition uPred_cmra_valid_eq :
   @uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux.
 
 Class BUpd (A : Type) : Type := bupd : A → A.
+Instance : Params (@bupd) 2.
 
 Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ k yf,
-- 
GitLab