From 3162a65275a7a8cb829025bde1486541f70757ac Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 26 Oct 2021 14:33:27 +0200
Subject: [PATCH] fractional_big_sep*: uniform type annotations

To match the suggestion in
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/737#note_75017.
---
 iris/bi/lib/fractional.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 997910f90..c310657d8 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -77,8 +77,8 @@ Section fractional.
     rewrite !assoc. f_equiv. by rewrite comm.
   Qed.
 
-  Global Instance fractional_big_sepL {A} l Ψ :
-    (∀ k (x : A), Fractional (Ψ k x)) →
+  Global Instance fractional_big_sepL {A} (l : list A) Ψ :
+    (∀ k x, Fractional (Ψ k x)) →
     Fractional (PROP:=PROP) (λ q, [∗ list] k↦x ∈ l, Ψ k x q)%I.
   Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed.
 
@@ -88,7 +88,7 @@ Section fractional.
   Proof. intros ? q q'. rewrite -big_sepL2_sep. by setoid_rewrite fractional. Qed.
 
   Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
-    (∀ k (x : A), Fractional (Ψ k x)) →
+    (∀ k x, Fractional (Ψ k x)) →
     Fractional (PROP:=PROP) (λ q, [∗ map] k↦x ∈ m, Ψ k x q)%I.
   Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
 
-- 
GitLab