From dbb44a4002c3c3d873f7a44673a4a71182b9c220 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Feb 2018 10:38:34 +0100
Subject: [PATCH] consistent non-parentheses for Implicit Types

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

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index f7b00a430..07c9185c8 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -62,7 +62,7 @@ Hint Mode BUpdFacts ! - : typeclass_instances.
 
 Section bupd_derived.
   Context `{BUpdFacts PROP}.
-  Implicit Types (P Q R: PROP).
+  Implicit Types P Q R: PROP.
 
   (* FIXME: Removing the `PROP:=` diverges. *)
   Global Instance bupd_proper : Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _.
@@ -119,7 +119,7 @@ Hint Mode FUpdFacts ! - - : typeclass_instances.
 
 Section fupd_derived.
   Context `{FUpdFacts PROP}.
-  Implicit Types (P Q R: PROP).
+  Implicit Types P Q R: PROP.
 
   Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
 
-- 
GitLab