Stop using auto with * in intuition

backend/Locations.v

@@ -488,7 +488,7 @@ Module OrderedLoc <: OrderedType.
     destruct H0. auto.
     destruct H.
     right.  split. auto.
-    intuition.
+    intuition try lia.
     right; split. congruence. eapply OrderedTyp.lt_trans; eauto.
   Qed.
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.

backend/ValueAnalysis.v

@@ -17,6 +17,8 @@ Require Import Values Memory Globalenvs Builtins Events.
 Require Import Registers Op RTL.
 Require Import ValueDomain ValueAOp Liveness.
 
+Local Ltac Tauto.intuition_solver ::= auto with exfalso bool va.
+
 (** * The dataflow analysis *)
 
 Definition areg (ae: aenv) (r: reg) : aval := AE.get r ae.

cfrontend/Cminorgenproof.v

@@ -22,6 +22,8 @@ Require Import Csharpminor Switch Cminor Cminorgen.
 
 Local Open Scope error_monad_scope.
 
+Local Ltac Tauto.intuition_solver ::= auto with exfalso.
+
 Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) :=
   match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp.
 

cfrontend/Cstrategy.v

@@ -34,6 +34,8 @@ Require Import Cop.
 Require Import Csyntax.
 Require Import Csem.
 
+Local Ltac Tauto.intuition_solver ::= auto with bool.
+
 Section STRATEGY.
 
 Variable ge: genv.

common/Events.v

@@ -27,6 +27,8 @@ Require Import Memory.
 Require Import Globalenvs.
 Require Import Builtins.
 
+Local Ltac Tauto.intuition_solver ::= auto with mem.
+
 (** Backwards compatibility for Hint Rewrite locality attributes. *)
 Set Warnings "-unsupported-attributes".
 

common/Memory.v

@@ -46,6 +46,8 @@ Local Unset Case Analysis Schemes.
 
 Local Notation "a # b" := (PMap.get b a) (at level 1).
 
+Local Ltac Tauto.intuition_solver ::= auto with zarith bool exfalso.
+
 Module Mem <: MEM.
 
 Definition perm_order' (po: option permission) (p: permission) :=

common/Smallstep.v

@@ -29,6 +29,8 @@ Require Import Integers.
 
 Set Implicit Arguments.
 
+Local Ltac Tauto.intuition_solver ::= auto with sets.
+
 (** * Closures of transitions relations *)
 
 Section CLOSURES.

lib/Floats.v

@@ -25,6 +25,8 @@ Require Import Program.
 Require Archi.
 Import ListNotations.
 
+Local Ltac Tauto.intuition_solver ::= auto with exfalso bool.
+
 Close Scope R_scope.
 Open Scope Z_scope.
 Set Asymmetric Patterns.

lib/Integers.v

@@ -20,6 +20,8 @@ Require Import Eqdep_dec Zquot Zwf.
 Require Import Coqlib Zbits.
 Require Archi.
 
+Local Ltac Tauto.intuition_solver ::= auto with zarith bool.
+
 (** Backwards compatibility for Hint Rewrite locality attributes. *)
 Set Warnings "-unsupported-attributes".
 

lib/Intv.v

@@ -21,6 +21,8 @@ Require Import Zwf.
 Require Coq.Program.Wf.
 Require Import Recdef.
 
+Local Ltac Tauto.intuition_solver ::= auto with zarith bool.
+
 Definition interv : Type := (Z * Z)%type.
 
 (** * Membership *)

lib/IntvSets.v

@@ -18,6 +18,8 @@
 
 Require Import Coqlib.
 
+Local Ltac Tauto.intuition_solver ::= auto with zarith bool.
+
 Module ISet.
 
 (** "Raw", non-dependent implementation.  A set of intervals is a

lib/Zbits.v

@@ -20,6 +20,8 @@
 Require Import Psatz Zquot.
 Require Import Coqlib.
 
+Local Ltac Tauto.intuition_solver ::= auto with crelations zarith bool.
+
 (** ** Modulo arithmetic *)
 
 (** We define and state properties of equality and arithmetic modulo a