diff --git a/ProofMode.md b/ProofMode.md
index e004d3595af54c5425ad534d6ae78233fd6147ac..b17ec1fc6073504b0a7dacda23631836ba789847 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -17,8 +17,8 @@ Applying hypotheses and lemmas
   conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
   proof mode terms below.
   If the applied term has more premises than given specialization patterns, the
-  pattern is extended with `[-] ... [-]`.  As a consequence, all unused spatial
-  hypotheses move to the first premise without an explicit specialization
+  pattern is extended with `[] ... []`.  As a consequence, all unused spatial
+  hypotheses move to the last premise without an explicit specialization
   pattern.
 
 Context management
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index af482f59e08f483248faeec14181824246130d6a..a5f79c5fe4ebbb2fe61137b360973e8af63ad7f5 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -431,7 +431,7 @@ Tactic Notation "iApply" open_constr(lem) :=
       [env_cbv; reflexivity
       |apply _
       |lazy beta (* reduce betas created by instantiation *)]
-    |iSpecializePat H "[-]"; last go H] in
+    |iSpecializePat H "[]"; last go H] in
   iPoseProofCore lem as false true (fun H =>
     first [iExact H|go H|iTypeOf H (fun Q => fail 1 "iApply: cannot apply" Q)]).
 
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index f8302508d70aec9fefcb30f7045fc9e7e0ecd195..28e5da973fabe6091e337a04d4edacb6beae5eb7 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -118,5 +118,5 @@ Proof.
 Qed.
 
 Lemma demo_11 (M : ucmraT) (P Q R : uPred M) :
-  (P -∗ Q -∗ True -∗ True -∗ R) -∗ P -∗ Q -∗ R.
+  (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
 Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed.