Tauto.intuition_solver has a sane default,

no need to redefine it any more
mit-plv · May 12, 2024 · 7d67a24 · 7d67a24
1 parent 309fe7e
commit 7d67a24
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/coqutil/sanity.v b/src/coqutil/sanity.v
@@ -1,3 +1,2 @@
 Global Unset Universe Minimization ToSet.
 Global Set Default Goal Selector "!".
-Ltac Tauto.intuition_solver ::= auto with core.