Merge branch 'persistent-fractional' into 'master'

persistent_fractional: strengthen like bi.persistent_sep_dup

See merge request iris/iris!717

CHANGELOG.md

@@ -77,6 +77,8 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add lemmas characterizing big-ops over pure predicates (`big_sep*_pure*`).
 * Move `BiAffine`, `BiPositive`, `BiLöb`, and `BiPureForall` from
   `bi.derived_connectives` to `bi.extensions`.
+* Strengthen `persistent_fractional` to support propositions that are persistent
+  and either affine or absorbing. (by Paolo G. Giarrusso, BedRock Systems)
 
 **Changes in `base_logic`:**
 

iris/bi/lib/fractional.v

@@ -65,8 +65,8 @@ Section fractional.
   Proof. intros. apply bi.wand_intro_r. by rewrite -(fractional_half P). Qed.
 
   (** Fractional and logical connectives *)
-  Global Instance persistent_fractional P :
-    Persistent P → Absorbing P → Fractional (λ _, P).
+  Global Instance persistent_fractional (P : PROP) :
+    Persistent P → TCOr (Affine P) (Absorbing P) → Fractional (λ _, P).
   Proof. intros ?? q q'. apply: bi.persistent_sep_dup. Qed.
 
   Global Instance fractional_sep Φ Ψ :