Commit 00b210d9 authored by Robbert Krebbers's avatar Robbert Krebbers

Hint database for subst.

parent eb82a9c7
......@@ -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
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment