diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 18c780e64dcf3c0445cd1f63f17560f8abce916d..ade36115e2ab9d9df32dc6c1f73b9fde89ec41ca 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -969,8 +969,8 @@ Tactic Notation "iModCore" constr(H) :=
   eapply tac_modal_elim with _ H _ _ _ _ _;
     [env_reflexivity || fail "iMod:" H "not found"
     |apply _ ||
-     let P := match goal with |- ElimModal ?P _ _ _ => P end in
-     let Q := match goal with |- ElimModal _ _ ?Q _ => Q end in
+     let P := match goal with |- ElimModal _ ?P _ _ _ => P end in
+     let Q := match goal with |- ElimModal _ _ _ ?Q _ => Q end in
      fail "iMod: cannot eliminate modality " P "in" Q
     |try fast_done (* optional side-condition *)
     |env_reflexivity|].