diff --git a/theories/tactics.v b/theories/tactics.v
index d5867ab6d90799e057fcc031ce9dc682005944e1..8a0551fb89a73076b660765f8e0069dca927cd15 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -26,10 +26,12 @@ Hint Extern 998 (_ = _) => f_equal : f_equal.
 Hint Extern 999 => congruence : congruence.
 Hint Extern 1000 => lia : lia.
 Hint Extern 1000 => omega : omega.
+Hint Extern 1001 => progress subst : subst. (** backtracking on this one will
+be very bad, so use with care! *)
 
 (** The tactic [intuition] expands to [intuition auto with *] by default. This
 is rather efficient when having big hint databases, or expensive [Hint Extern]
-declarations as the above. *)
+declarations as the ones above. *)
 Tactic Notation "intuition" := intuition auto.
 
 (** A slightly modified version of Ssreflect's finishing tactic [done]. It