From 95fd712afc099c6ce382f93bcce09cba9e284ba4 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Sun, 2 Mar 2025 13:58:12 +0100
Subject: [PATCH] Fixed lib.fixpoint in do_lob

---
 diaframe/lib/do_lob.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/diaframe/lib/do_lob.v b/diaframe/lib/do_lob.v
index 764ae6a1..cea460dd 100644
--- a/diaframe/lib/do_lob.v
+++ b/diaframe/lib/do_lob.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi telescopes lib.laterable lib.fixpoint.
+From iris.bi Require Export bi telescopes lib.laterable lib.fixpoint_mono.
 From iris.proofmode Require Import proofmode environments.
 From diaframe Require Import proofmode_base utils_ltac2.
 
-- 
GitLab