From 5b4262a1a139f039bcc7408cf41b21394d77eab9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Wed, 26 Mar 2025 15:39:02 +0100
Subject: [PATCH] add missing instances + group more sensibly

---
 lifetime/lifetime_sig.v      | 9 +++++++--
 lifetime/model/definitions.v | 1 +
 lifetime/model/primitive.v   | 2 ++
 3 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v
index 095c9560..451a0727 100644
--- a/lifetime/lifetime_sig.v
+++ b/lifetime/lifetime_sig.v
@@ -67,7 +67,14 @@ Module Type lifetime_sig.
   Global Declare Instance lft_inhabited : Inhabited lft.
   Global Declare Instance lft_eq_dec : EqDecision lft.
   Global Declare Instance lft_countable : Countable lft.
+
+  Global Declare Instance atomic_lft_inhabited : Inhabited atomic_lft.
+  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
+  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
+
   Global Declare Instance bor_idx_inhabited : Inhabited bor_idx.
+  Global Declare Instance bor_idx_eq_dec : EqDecision bor_idx.
+  Global Declare Instance bor_idx_countable : Countable bor_idx.
 
   Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
   Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
@@ -112,8 +119,6 @@ Module Type lifetime_sig.
   Global Declare Instance atomic_lft_to_lft_inj : Inj eq eq atomic_lft_to_lft.
   Global Declare Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 
-  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
-  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
 
   (** * Laws *)
   Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v
index ee360cda..35fdc4a0 100644
--- a/lifetime/model/definitions.v
+++ b/lifetime/model/definitions.v
@@ -353,6 +353,7 @@ Qed.
 Global Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 Proof. apply _. Qed.
 
+Global Definition atomic_lft_inhabited : Inhabited atomic_lft := _.
 Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
 Global Definition atomic_lft_countable : Countable atomic_lft := _.
 End basic_properties.
diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 4f32bf11..a9104e8f 100644
--- a/lifetime/model/primitive.v
+++ b/lifetime/model/primitive.v
@@ -306,6 +306,8 @@ Local Instance lft_inhabited : Inhabited lft := _.
 Local Instance lft_eq_dec : EqDecision lft := _.
 Local Instance lft_countable : Countable lft := _.
 Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Local Instance bor_idx_eq_dec : EqDecision bor_idx := _.
+Local Instance bor_idx_countable : Countable bor_idx := _.
 Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
-- 
GitLab