From 74f173153680013a35d7d229333c82fe164ccd7c Mon Sep 17 00:00:00 2001 From: Ike Mulder <ikemulder@hotmail.com> Date: Sun, 2 Mar 2025 14:08:15 +0100 Subject: [PATCH] Another bot -> invalid rename --- diaframe/lib/own/proofmode_instances.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/diaframe/lib/own/proofmode_instances.v b/diaframe/lib/own/proofmode_instances.v index 6622ed9e..e4bd391e 100644 --- a/diaframe/lib/own/proofmode_instances.v +++ b/diaframe/lib/own/proofmode_instances.v @@ -383,7 +383,7 @@ Section recursive. by iRewrite "Ha". Qed. Global Instance sum_inl_inr_invalid_op {A B : cmra} (a : A) (b : B) Σ : - IsValidOp (CsumBot) (Cinl (B := B) a) (Cinr (A := A) b) Σ False. + IsValidOp (CsumInvalid) (Cinl (B := B) a) (Cinr (A := A) b) Σ False. Proof. split; rewrite /op /= /cmra_op //=; eauto. (* TODO: need proper access to unsealing lemma's *) uPred_primitive.unseal. @@ -391,7 +391,7 @@ Section recursive. rewrite /validN /= /cmra_validN //=. Qed. Global Instance sum_inr_inl_invalid_op {A B : cmra} (a : A) (b : B) Σ : - IsValidOp (CsumBot) (Cinr (A := B) a) (Cinl (B := A) b) Σ False. + IsValidOp (CsumInvalid) (Cinr (A := B) a) (Cinl (B := A) b) Σ False. Proof. split; rewrite /op /= /cmra_op //=; eauto. uPred_primitive.unseal. @@ -660,7 +660,7 @@ Section recursive. Qed. Global Instance excl_valid_op {O : ofe} (a1 a2 : excl O) Σ: - IsValidOp ExclBot a1 a2 Σ False%I. + IsValidOp ExclInvalid a1 a2 Σ False%I. Proof. split; rewrite excl_validI /=; eauto. Qed. Global Instance excl_included_merge {O : ofe} (o1 o2 : excl O) {Σ} : IsIncludedMerge o1 o2 (Σ := Σ) False%I. @@ -1029,4 +1029,4 @@ Section recursive. iSplit => //. Qed. -End recursive. \ No newline at end of file +End recursive. -- GitLab