diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v index e1a37c5765349e74506f82bcff2de9949bc33c06..b38a3094ddd7f12ff197238fa2da99bb751af4c2 100644 --- a/iris/proofmode/class_instances_later.v +++ b/iris/proofmode/class_instances_later.v @@ -190,7 +190,7 @@ Global Instance from_forall_later {A} P (Φ : A → PROP) name : Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed. Global Instance from_forall_laterN {A} P (Φ : A → PROP) n name : - FromForall P Φ name → FromForall (▷^n P) (λ a, ▷^n (Φ a))%I name. + FromForall P Φ name → FromForall (▷^n P) (λ a, ▷^n (Φ a))%I name. Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed. Global Instance from_forall_except_0 {A} P (Φ : A → PROP) name :