diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v index 72655d98556c61b309979a49c0f1128766d4ff41..898dc03abd000bd624dcd396fedd33e2941d2646 100644 --- a/theories/algebra/auth.v +++ b/theories/algebra/auth.v @@ -8,6 +8,9 @@ Add Printing Constructor auth. Arguments Auth {_} _ _. Arguments authoritative {_} _. Arguments auth_own {_} _. +Instance: Params (@Auth) 1. +Instance: Params (@authoritative) 1. +Instance: Params (@auth_own) 1. Notation "◯ a" := (Auth None a) (at level 20). Notation "◠a" := (Auth (Excl' a) ∅) (at level 20).