Commit ed383a77 authored by Ralf Jung's avatar Ralf Jung

Make everything compile with Coq 8.6

parent a5f94780
...@@ -2234,7 +2234,12 @@ Section Forall_Exists. ...@@ -2234,7 +2234,12 @@ Section Forall_Exists.
Lemma not_Forall_Exists l : ¬Forall P l Exists (not P) l. Lemma not_Forall_Exists l : ¬Forall P l Exists (not P) l.
Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed. Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed.
Lemma not_Exists_Forall l : ¬Exists P l Forall (not P) l. 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) := Global Instance Forall_dec l : Decision (Forall P l) :=
match Forall_Exists_dec dec l with match Forall_Exists_dec dec l with
| left H => left H | left H => left H
......
...@@ -52,7 +52,8 @@ Section ndisjoint. ...@@ -52,7 +52,8 @@ Section ndisjoint.
Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y. Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y.
Proof. Proof.
intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq. intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
intros [qx ->] [qy]. by intros [= ?%encode_inj]%list_encode_suffix_eq. intros [qx ->] [qy Hqy].
revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
Qed. Qed.
Lemma ndot_preserve_disjoint_l N E x : nclose N E nclose (N .@ x) E. Lemma ndot_preserve_disjoint_l N E x : nclose N E nclose (N .@ x) E.
......
...@@ -834,7 +834,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) := ...@@ -834,7 +834,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
| ESelName ?p ?H :: ?Hs => | ESelName ?p ?H :: ?Hs =>
iRevert H; go Hs; iRevert H; go Hs;
let H' := let H' :=
match p with true => constr:[IAlwaysElim (IName H)] | false => H end in match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
iIntros H' iIntros H'
end in end in
iElaborateSelPat Hs go. iElaborateSelPat Hs go.
......
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