From 760df7a12e44bb4a530c6601f61457a3e6c6a77d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 1 Jun 2018 16:17:27 +0200
Subject: [PATCH] fix remaining warnings

---
 theories/examples/circ_buffer.v | 2 +-
 theories/examples/kvnode.v      | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index ae0751d3..7eb1ee6b 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 9f2aa989..d3355c64 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.
-- 
GitLab