make iApply greatest_fixpoint_paco work in more cases

iris/bi/lib/fixpoint.v

@@ -312,7 +312,7 @@ Section greatest_coind.
   Qed.
   Local Existing Instance paco_mono.
 
-  Lemma greatest_fixpoint_paco `{!NonExpansive Φ} :
+  Lemma greatest_fixpoint_paco (Φ : A → PROP) `{!NonExpansive Φ} :
     □ (∀ y, Φ y -∗ F (bi_greatest_fixpoint (λ Ψ a, Φ a ∨ F Ψ a)) y) -∗
     ∀ x, Φ x -∗ bi_greatest_fixpoint F x.
   Proof using Type*.

tests/fixpoint.v

+From iris.bi Require Import lib.fixpoint.
+From iris.proofmode Require Import proofmode.
+From iris.prelude Require Import options.
+
+Section fixpoint.
+  Context {PROP : bi} `{!BiInternalEq PROP}
+    {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+
+  Definition L := bi_least_fixpoint F.
+  Definition G := bi_greatest_fixpoint F.
+
+  (* Make sure the lemmas apply without having to repeat the induction predicate [Φ]. *)
+  Lemma ind_test (a : A) :
+    ∀ x, L x -∗ x ≡ a.
+  Proof.
+    iApply (least_fixpoint_ind F); first by solve_proper. Undo.
+    iApply (least_fixpoint_ind_wf F); first by solve_proper. Undo.
+  Abort.
+
+  Lemma coind_test (a : A) :
+    ∀ x, x ≡ a -∗ G x.
+  Proof.
+    iApply (greatest_fixpoint_coind F); first by solve_proper. Undo.
+    iApply (greatest_fixpoint_paco F); first by solve_proper. Undo.
+  Abort.
+
+End fixpoint.