From 84227fa4f328e29d96b770161629122bf533ae02 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 8 Jun 2017 13:11:24 +0200
Subject: [PATCH] Params instances for auth.

---
 theories/algebra/auth.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 72655d985..898dc03ab 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).
 
-- 
GitLab