From f2fe3041735637e09bd06163f16a9035acf6c63c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Jun 2018 13:14:27 +0200
Subject: [PATCH] More Implicit Types.

---
 theories/bi/lib/laterable.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/bi/lib/laterable.v b/theories/bi/lib/laterable.v
index 46252fb51..a1243539d 100644
--- a/theories/bi/lib/laterable.v
+++ b/theories/bi/lib/laterable.v
@@ -11,7 +11,8 @@ Hint Mode Laterable + ! : typeclass_instances.
 
 Section instances.
   Context {PROP : sbi}.
-  Implicit Type (P : PROP).
+  Implicit Types P : PROP.
+  Implicit Types Ps : list PROP.
 
   Global Instance later_laterable P : Laterable (â–· P).
   Proof.
@@ -54,6 +55,6 @@ Section instances.
   Global Instance big_sepL_laterable Ps :
     Timeless (PROP:=PROP) emp →
     TCForall Laterable Ps →
-    Laterable (PROP:=PROP) ([∗] Ps).
+    Laterable ([∗] Ps).
   Proof. induction 2; simpl; apply _. Qed.
 End instances.
-- 
GitLab