Params instances for auth.

84227fa4 · Robbert Krebbers · d7bf36da · 84227fa4
Commit 84227fa4 authored Jun 08, 2017 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

theories/algebra/auth.v theories/algebra/auth.v +3 -0

No files found.
--- 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).