blob: abacfa5803595a2eae9b06cb85bdb0c77382c3f9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(** * Fixes *)
(** Coq is poorly designed in some ways. We fix some of these issues
in this file. *)
(** [intuition] means [intuition auto with *]. This is very wrong and
fragile and slow. We make [intuition] mean [intuition auto]. *)
Tactic Notation "intuition" tactic3(tactic) := intuition tactic.
Tactic Notation "intuition" := intuition auto.
(** A version of [intuition] that allows you to see how the old
[intuition] tactic solves the proof. *)
Ltac debug_intuition := idtac "<infomsg>Warning: debug_intuition should not be used in production code.</infomsg>"; intuition debug auto with *.
|
