Commit 9eb8cd13 authored by Ralf Jung's avatar Ralf Jung

fix build for Coq 8.10

parent ec592463
......@@ -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
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment