diff --git a/prelude/list.v b/prelude/list.v
index b96edfdc932616582df580d060c2a4aa16927024..c8af713f336f94f9896f192378695f4999573466 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 62de7e675a7c276c1ba2a9c1544b1e17739372f6..06b91c92cac4b5e3d07ec34e55bfd8a7b98037d0 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 c63a655e1b9d3f06b9c3c6886ea170f0e8580b4d..9941b50efd827ebcdb84161f6e05c189b8e87cff 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.