diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v index c6c897cbe4b616d6563585a1e3ea14a608812780..35c2e3f5f03116ed6d36042ea7dab2005890e8f7 100644 --- a/theories/base_logic/derived.v +++ b/theories/base_logic/derived.v @@ -672,9 +672,9 @@ Proof. Qed. (* Later derived *) -Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q. +Lemma later_proper' P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q. Proof. by intros ->. Qed. -Hint Resolve later_mono later_proper. +Hint Resolve later_mono later_proper'. Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M). Proof. intros P Q; apply later_mono. Qed. Global Instance later_flip_mono' : diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v index 6796f5a440b1cfd9e874f33dd604c6577977d8a1..46768bd2e7ef7b26a0f3bd238585a00ed994747e 100644 --- a/theories/base_logic/primitive.v +++ b/theories/base_logic/primitive.v @@ -307,7 +307,8 @@ Proof. unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega. apply HPQ; eauto using cmra_validN_S. Qed. -Global Instance later_proper' : +Definition later_ne : NonExpansive (@uPred_later M) := _. +Global Instance later_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _. Global Instance plainly_ne : NonExpansive (@uPred_plainly M). Proof.