Hint database for subst.

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