From 1b2301d2654450b99de60da9f41785580ed64df3 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:34:38 +0100
Subject: [PATCH] move instances

---
 lifetime/model/definitions.v | 4 ----
 lifetime/model/primitive.v   | 2 ++
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v
index 900aad50..ee360cda 100644
--- a/lifetime/model/definitions.v
+++ b/lifetime/model/definitions.v
@@ -355,8 +355,4 @@ Proof. apply _. Qed.
 
 Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
 Global Definition atomic_lft_countable : Countable atomic_lft := _.
-
-Global Definition lft_eq_dec : EqDecision lft := _.
-Global Definition lft_countable : Countable lft := _.
-
 End basic_properties.
diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v
index 3fd9472c..4f32bf11 100644
--- a/lifetime/model/primitive.v
+++ b/lifetime/model/primitive.v
@@ -303,6 +303,8 @@ Qed.
 
 (** Basic rules about lifetimes  *)
 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 lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
-- 
GitLab