diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v index c83392c9eed3adad303072f6d416404f54a4cf8c..195a6040bab97a882e56708c6f324911145aff71 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,