diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v index 47bb349fa8d85475fc4ee3a320354afa8fd4e7aa..99aa1c5d21dd5ecd6c39a930ff8d993b567bdb68 100644 --- a/theories/algebra/ufrac_auth.v +++ b/theories/algebra/ufrac_auth.v @@ -41,8 +41,8 @@ Definition ufrac_auth_frag {A : cmraT} (q : Qp) (x : A) : ufrac_authR A := Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag. -Instance: Params (@ufrac_auth_auth) 2. -Instance: Params (@ufrac_auth_frag) 2. +Instance: Params (@ufrac_auth_auth) 2 := {}. +Instance: Params (@ufrac_auth_frag) 2 := {}. Notation "â—U{ q } a" := (ufrac_auth_auth q a) (at level 10, format "â—U{ q } a"). Notation "â—¯U{ q } a" := (ufrac_auth_frag q a) (at level 10, format "â—¯U{ q } a").