From 1df7edd5a70f3614c4551ec57c84b959d032b978 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 19 Nov 2022 15:44:32 -0500 Subject: [PATCH] Garbage-collect options in sanity.v --- src/coqutil/sanity.v | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/src/coqutil/sanity.v b/src/coqutil/sanity.v index 499905b4..fc068f3d 100644 --- a/src/coqutil/sanity.v +++ b/src/coqutil/sanity.v @@ -1,18 +1,3 @@ Global Unset Universe Minimization ToSet. Global Set Default Goal Selector "!". - -(** Work around some counter-intuitive defaults. *) - -(** [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. - -(** [firstorder] means [firstorder auto with *]. This is very wrong - and fragile and slow. We make [firstorder] mean [firstorder - auto]. *) -Global Set Firstorder Solver auto. - -(** A version of [intuition] that allows you to see how the old - [intuition] tactic solves the proof. *) -Ltac debug_intuition := idtac "Warning: debug_intuition should not be used in production code."; intuition debug auto with *. +Ltac Tauto.intuition_solver ::= auto with core.