diff --git a/algebra/upred.v b/algebra/upred.v index 4a0c0817b381fee76f7bc937926d6595343f7e1c..1ff6dfcbc814c106bb3dccc1a8c754eafd90de0f 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -301,7 +301,7 @@ Proof. by intros n Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed. Global Instance forall_proper A : Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_forall M A). Proof. by intros Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed. -Global Instance exists_ne A : +Global Instance exist_ne A : Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A). Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed. Global Instance exist_proper A : diff --git a/program_logic/invariants.v b/program_logic/invariants.v index 559e4ba2b34ee8baeb62166c87cc00d3dcae7f68..a8b4269559d8af55a30a1ce40fc6406ce2825470 100644 --- a/program_logic/invariants.v +++ b/program_logic/invariants.v @@ -21,7 +21,7 @@ Implicit Types P Q R : iProp Λ Σ. Implicit Types Φ : val Λ → iProp Λ Σ. Global Instance inv_contractive N : Contractive (@inv Λ Σ N). -Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed. +Proof. intros n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive. Qed. Global Instance inv_always_stable N P : AlwaysStable (inv N P). Proof. rewrite /inv; apply _. Qed.