From 0ef88ec628ec27bf77906f29881882a061d20c58 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 8 Feb 2016 21:19:19 +0100
Subject: [PATCH] Hint database for subst.

---
 theories/tactics.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index d5867ab6..8a0551fb 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
-- 
GitLab