Merge pull request #37 from JasonGross/fix-intuition

Redesign intuition, speeding up overall compilation by 20%

1 files changed, 13 insertions, 0 deletions

diff --git a/src/Util/FixCoqMistakes.v b/src/Util/FixCoqMistakes.v
new file mode 100644
index 000000000..abacfa580
--- /dev/null
+++ b/src/Util/FixCoqMistakes.v
@@ -0,0 +1,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 *.