blob: 129344f8341ba5a68b19e2a03d68835d69c8e9aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(** * Fixes *)
Require Export Crypto.Util.GlobalSettings.
(** 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 *.
|
