firstorder: default tactic is “auto with core”

6 files changed, 16 insertions, 12 deletions

diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v
index d628456c78..ee4bac3542 100644
--- a/theories/Compat/Coq812.v
+++ b/theories/Compat/Coq812.v
@@ -9,3 +9,4 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.12 *)
+Set Firstorder Solver auto with *.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index d267991c3c..73021a84a3 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -772,7 +772,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     generalize C; unfold compat_bool, Proper, respectful; intros; apply (f_equal negb);
      auto.
     simpl; unfold Equal; intuition.
-    apply filter_3; firstorder.
+    apply filter_3; firstorder with bool.
     elim (H2 a); intros.
     assert (In a s).
      eapply filter_1; eauto.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 6a1554d102..f050f11170 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1413,13 +1413,16 @@ End Fold_Right_Recursor.
     Lemma existsb_exists :
       forall l, existsb l = true <-> exists x, In x l /\ f x = true.
     Proof.
-      induction l; simpl; intuition.
-      inversion H.
-      firstorder.
-      destruct (orb_prop _ _ H1); firstorder.
-      firstorder.
-      subst.
-      rewrite H2; auto.
+      induction l as [ | a m IH ]; split; simpl.
+      - easy.
+      - intros [x [[]]].
+      - rewrite orb_true_iff; intros [ H | H ].
+        + exists a; auto.
+        + rewrite IH in H; destruct H as [ x [ Hxm Hfx ] ].
+          exists x; auto.
+      - intros [ x [ [ Hax | Hxm ] Hfx ] ].
+        + now rewrite Hax, Hfx.
+        + destruct IH as [ _ -> ]; eauto with bool.
     Qed.
 
     Lemma existsb_nth : forall l n d, n < length l ->
@@ -2747,7 +2750,7 @@ Section Exists_Forall.
     Proof.
       split.
       - induction 1; firstorder; subst; auto.
-      - induction l; firstorder.
+      - induction l; firstorder auto with datatypes.
     Qed.
 
     Lemma Forall_nth l :
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index a15b533d3d..4f2f4256e2 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -771,7 +771,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
     unfold Exists, In. intro f.
     induction s as [|l IHl o r IHr]; intros i; simpl.
-     firstorder.
+     firstorder with bool.
      rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
       split.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 6af9572fff..7c5b43096a 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -60,7 +60,7 @@ Ltac zcongruence := repeat red; intros; zify; congruence.
 
 Instance eq_equiv : Equivalence eq.
 Proof.
-  split. 1-2: firstorder.
+  split. 1-2: firstorder auto with crelations.
   intros x y z; apply eq_trans.
 Qed.
 
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v
index 6e8d9e4571..fe9794de8a 100644
--- a/theories/Structures/EqualitiesFacts.v
+++ b/theories/Structures/EqualitiesFacts.v
@@ -74,7 +74,7 @@ Module KeyDecidableType(D:DecidableType).
  Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) :
   InA eqk p m -> exists q, eqk p q /\ InA eqke q m.
  Proof.
-  induction 1; firstorder.
+  induction 1; firstorder auto with crelations.
  Qed.
 
  Lemma InA_eqk {elt} p q (m:list (key*elt)) :