10 files changed, 28 insertions, 15 deletions
diff --git a/doc/changelog/04-tactics/11760-firstorder-leaf.rst b/doc/changelog/04-tactics/11760-firstorder-leaf.rst
new file mode 100644
index 0000000000..e6e4b827e5
--- /dev/null
+++ b/doc/changelog/04-tactics/11760-firstorder-leaf.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+  The default tactic used by :g:`firstorder` is
+  :g:`auto with core` instead of :g:`auto with *`;
+  see :ref:`decisionprocedures` for details;
+  old behavior can be reset by using the `-compat 8.12` command-line flag;
+  to ease the migration of legacy code, the default solver can be set to `debug auto with *`
+  with `Set Firstorder Solver debug auto with *`
+  (`#11760 <https://github.com/coq/coq/pull/11760>`_,
+  by Vincent Laporte).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index be185e885b..d498c1ee2c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4286,7 +4286,7 @@ some incompatibilities.
    :name: Firstorder Solver
 
    The default tactic used by :tacn:`firstorder` when no rule applies is
-   :g:`auto with *`, it can be reset locally or globally using this option.
+   :g:`auto with core`, it can be reset locally or globally using this option.
 
    .. cmd:: Print Firstorder Solver
 
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 0133a02ca7..49e4c91182 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -47,7 +47,7 @@ let ()=
 
 
 let default_intuition_tac =
-  let tac _ _ = Auto.h_auto None [] None in
+  let tac _ _ = Auto.h_auto None [] (Some []) in
   let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
   let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
   Tacenv.register_ml_tactic name [| tac |];
diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v
index 9cf6879699..7abbe29452 100644
--- a/test-suite/output/NoAxiomFromR.v
+++ b/test-suite/output/NoAxiomFromR.v
@@ -5,6 +5,6 @@ Inductive TT : Set :=
 
 Lemma lem4 : forall (n m : nat),
 S m <= m -> C (S m) <> C n -> False.
-Proof. firstorder. Qed.
+Proof. firstorder lia. Qed.
 
 Print Assumptions lem4.
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)) :