From 265c2a1343ec422e0c209400d800781b9f024e1e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 11 Jun 2019 16:36:23 +0200
Subject: [PATCH] Fix compilation with Coq master.

---
 theories/algebra/ufrac_auth.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v
index 47bb349fa..99aa1c5d2 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").
-- 
GitLab