From ad2e80d6434fe36e0e49ad457c89e81dc9fcc95c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Mar 2020 23:26:27 +0100
Subject: [PATCH] Compilation fixes.

Fix both an error by my, and a provide compatibility with older Coq versions
whose `lia` is less powerful.
---
 theories/finite.v | 2 +-
 theories/list.v   | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/finite.v b/theories/finite.v
index 93292786..d6ef2254 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -208,7 +208,7 @@ Section enc_finite.
     apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj.
     destruct (seq _ _ !! i) as [i'|] eqn:Hi',
       (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
-    destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst.
+    apply lookup_seq in Hi' as  [-> ?]. apply lookup_seq in Hj' as [-> ?].
     rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal.
   Qed.
   Next Obligation.
diff --git a/theories/list.v b/theories/list.v
index 03660b3f..4d70d994 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3725,7 +3725,8 @@ Section seqZ.
     Forall P (seqZ m n) ↔ ∀ m', m ≤ m' < m + n → P m'.
   Proof.
     rewrite Forall_lookup. split.
-    - intros H j [??]. apply (H (Z.to_nat (j - m))), lookup_seqZ. lia.
+    - intros H j [??]. apply (H (Z.to_nat (j - m))), lookup_seqZ.
+      rewrite !Z2Nat.id by lia. lia.
     - intros H j x [-> ?]%lookup_seqZ. auto with lia.
   Qed.
 End seqZ.
-- 
GitLab