From 3b9f9c3b07122ab6604be16fa1d412e626575c15 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Thu, 13 Oct 2016 10:59:48 +0200
Subject: [PATCH] Make everything compile with Coq 8.6
---
theories/list.v | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/theories/list.v b/theories/list.v
index bcd3c29..7500abe 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2234,7 +2234,12 @@ Section Forall_Exists.
Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed.
Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
- Proof. by destruct (Forall_Exists_dec (λ x, swap_if (decide (P x))) l). Qed.
+ Proof.
+ (* TODO: Coq 8.6 needs type annotation here, Coq 8.5 did not.
+ Should we report this? *)
+ by destruct (@Forall_Exists_dec (not ∘ P) _
+ (λ x : A, swap_if (decide (P x))) l).
+ Qed.
Global Instance Forall_dec l : Decision (Forall P l) :=
match Forall_Exists_dec dec l with
| left H => left H
--
GitLab