itauto tactic notation with omitted leaf
In Coq as of early 2022, intuition.
means intuition (auto with *)
. When using the Stdpp library as we do, the behavior of intuition.
is changed to the more sane intuition auto.
In order to make Itauto a more drop-in replacement for intuition, how about adding a Stdpp-like tactic notation that makes itauto.
behave like itauto auto.
?
Here is the diff, which I would be happy to submit as a PR if given access:
diff --git a/theories/Itauto.v b/theories/Itauto.v
index 349c422..9c456ea 100644
--- a/theories/Itauto.v
+++ b/theories/Itauto.v
@@ -68,6 +68,8 @@ Tactic Notation "itauto" tactic(tac) :=
gen_conflicts tac ;
vitautog.
+Tactic Notation "itauto" :=
+ itauto auto.
Ltac itautor tac := let t := solve[tac | itauto tac] in itauto t.