diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 75d192389d9f7e355620a6795897770a209cb8ad..e01b3678292ed6247d4b42e1145b2ef8deefd5ab 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1341,6 +1341,8 @@ Tactic Notation "iModIntro" uconstr(sel) :=
     |pm_prettify (* reduce redexes created by instantiation *)
      (* subgoal *) ].
 Tactic Notation "iModIntro" := iModIntro _.
+
+(** DEPRECATED *)
 Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)