More Implicit Types.

f2fe3041 · Robbert Krebbers · ffd67c09 · f2fe3041
Commit f2fe3041 authored Jun 29, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 2 deletions

theories/bi/lib/laterable.v theories/bi/lib/laterable.v +3 -2

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