diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index ae0751d3dc32a25ef8dba114056b2c34c6bc2a25..7eb1ee6b22e4f51cab3d1d361fb8e98d8bcfc1b9 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -309,7 +309,7 @@ Section CircBuffer.
         iSplitR "P"; last by iRight.
         iExists γ, i, j.
         iFrame "pToks pW cR2". iPureIntro.
-        eapply Zlt_le_trans; first exact H. by apply Zplus_le_compat_r, inj_le.
+        eapply Z.lt_le_trans; first exact H. by apply Zplus_le_compat_r, inj_le.
 
       - wp_if_false.
         wp_bind ([_]_na <- _)%E. wp_op. wp_op.
diff --git a/theories/examples/kvnode.v b/theories/examples/kvnode.v
index 9f2aa9893b29434b2e0cb891dc785a86878f8b94..d3355c6474347c765e26b5e7f84b611ef6dfbf60 100644
--- a/theories/examples/kvnode.v
+++ b/theories/examples/kvnode.v
@@ -6,6 +6,8 @@ From igps Require Import persistor viewpred proofmode weakestpre protocols singl
   invariants fork.
 From igps.gps Require Import shared plain recursive.
 From igps.examples Require Import abs_hashtable snapshot hist_protocol repeat for_loop list_lemmas.
+Require Recdef.
+
 Import uPred lang.base.
 
 Section kvnode.
@@ -287,7 +289,7 @@ Section proof.
     rewrite !is_Some_alt; destruct (m !! n'); done.
   Qed.
 
-  Require Import Recdef.
+  Import Recdef.
 
   Function make_log {A} (n : nat) (d : A) { measure id n } : gmap nat A :=
     <[n := d]>match n with O => ∅ | _ => (make_log (n - 2) d) end.