From 9eb8cd1389e664c35aeab575cb8b2db461d735b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Jul 2019 15:13:36 +0200
Subject: [PATCH] fix build for Coq 8.10
---
theories/decidable.v | 3 +++
theories/list.v | 4 +++-
2 files changed, 6 insertions(+), 1 deletion(-)
diff --git a/theories/decidable.v b/theories/decidable.v
index 925a6b86..c5db311f 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -94,6 +94,9 @@ Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Lemma bool_decide_decide P `{!Decision P} :
bool_decide P = if decide P then true else false.
Proof. reflexivity. Qed.
+Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
+ (if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
+Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
Tactic Notation "case_bool_decide" "as" ident (Hd) :=
match goal with
diff --git a/theories/list.v b/theories/list.v
index f79766d5..b853eb94 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -921,7 +921,9 @@ Section find.
list_find P l = list_find Q l.
Proof.
intros HPQ. induction l as [|x l IH]; [done|]. simpl.
- erewrite decide_iff by done. by rewrite IH.
+ rewrite !decide_bool_decide.
+ rewrite (bool_decide_iff _ (Q x)) by done.
+ rewrite IH. done.
Qed.
End find.
--
GitLab