From ed383a7740adbde57f5b210e83268786e52a3f22 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 Oct 2016 10:59:48 +0200
Subject: [PATCH] Make everything compile with Coq 8.6
---
prelude/list.v | 7 ++++++-
program_logic/namespaces.v | 3 ++-
proofmode/tactics.v | 2 +-
3 files changed, 9 insertions(+), 3 deletions(-)
diff --git a/prelude/list.v b/prelude/list.v
index b96edfdc9..c8af713f3 100644
--- a/prelude/list.v
+++ b/prelude/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
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 62de7e675..06b91c92c 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -52,7 +52,8 @@ Section ndisjoint.
Lemma ndot_ne_disjoint N x y : x ≠y → N .@ x ⊥ N .@ y.
Proof.
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.
Lemma ndot_preserve_disjoint_l N E x : nclose N ⊥ E → nclose (N .@ x) ⊥ E.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index c63a655e1..9941b50ef 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -834,7 +834,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
| ESelName ?p ?H :: ?Hs =>
iRevert H; go Hs;
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'
end in
iElaborateSelPat Hs go.
--
GitLab