diff --git a/diaframe/lib/do_lob.v b/diaframe/lib/do_lob.v index 764ae6a19107a482f3180fc2e01cf9f4f7014525..cea460ddc7633fe117e2f40f48ef62ec27343c23 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.