From a7c4d317bb9516fd94fee195cbd959551b3670f5 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sun, 2 Mar 2025 13:48:56 +0100
Subject: [PATCH] Bot -> Invalid rename, fixpoint move

---
 diaframe/lib/greatest_fixpoint.v | 2 +-
 diaframe/lib/own_hints.v         | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/diaframe/lib/greatest_fixpoint.v b/diaframe/lib/greatest_fixpoint.v
index 47603039..20a5318b 100644
--- a/diaframe/lib/greatest_fixpoint.v
+++ b/diaframe/lib/greatest_fixpoint.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi telescopes lib.fixpoint.
+From iris.bi Require Export bi telescopes lib.fixpoint_mono.
 From iris.proofmode Require Import proofmode environments classes_make.
 From diaframe Require Import proofmode_base.
 
diff --git a/diaframe/lib/own_hints.v b/diaframe/lib/own_hints.v
index eab37a4a..6db9f939 100644
--- a/diaframe/lib/own_hints.v
+++ b/diaframe/lib/own_hints.v
@@ -335,7 +335,7 @@ From stdpp Require Import telescopes.
 Section other.
 
   Global Instance excl_inhabited {A : ofe} : Inhabited (exclR A).
-  Proof. split. by apply ExclBot. Qed.
+  Proof. split. by apply ExclInvalid. Qed.
 
   Global Arguments option_unit_instance /.
 
@@ -998,14 +998,14 @@ Section validity.
       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.
       rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
       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.
       rewrite uPred_cmra_valid_eq /= /uPred_cmra_valid_def /=.
@@ -1482,7 +1482,7 @@ Section validity.
     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. *)
     Lemma excl_subtract {O : ofe} (o1 o2 : O) : (* this one is bad for recursive instances *)
       TCIf (SolveSepSideCondition (¬ (o1 ≡ o2))) False TCTrue →
-- 
GitLab