diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v index 997910f90c0e6bac9781c4d4f526e7bec09abf75..c310657d84a9d4c4266d2286e8f70b09257d1a2d 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.