fix remaining warnings

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.

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.