Commit 3b9f9c3b authored by Ralf Jung's avatar Ralf Jung
Browse files

Make everything compile with Coq 8.6

parent 62389c82
......@@ -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.
(* 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).
Global Instance Forall_dec l : Decision (Forall P l) :=
match Forall_Exists_dec dec l with
| left H => left H
Supports Markdown
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