Default intuition solver is now auto

doc/changelog/04-tactics/17811-intuit-auto.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  the default ``intuition_solver`` (see
+  :tacn:`intuition`) is now :tacn:`auto` instead of `auto with *`
+  (`#17811 <https://github.com/coq/coq/pull/17811>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proofs/automatic-tactics/logic.rst

@@ -58,14 +58,10 @@ Solvers for logic and equality
    simpler than it) and applies :n:`@ltac_expr` to them :cite:`Mun94`. If
    :n:`@ltac_expr` is not specified, it defaults to ``Tauto.intuition_solver``.
 
-   The initial value of ``intuition_solver`` is equivalent to :n:`auto
-   with *` but prints warning ``intuition-auto-with-star`` when it
-   solves a goal that :tacn:`auto` cannot solve. In a future version
-   it will be changed to just :tacn:`auto`. Use ``intuition tac``
-   locally or ``Ltac Tauto.intuition_solver ::= tac`` globally to
-   silence the warning in a forward compatible way with your choice of
-   tactic ``tac`` (``auto``, ``auto with *``, ``auto with`` your
-   prefered databases, or any other tactic).
+   The default value of ``intuition_solver`` is :tacn:`auto`. Use
+   ``intuition tac`` or ``Ltac Tauto.intuition_solver ::= tac`` to use
+   your choice of tactic ``tac`` instead (``auto``, ``auto with *``,
+   ``auto with`` your prefered databases, or any other tactic).
 
    If :n:`@ltac_expr` fails on some goals then :tacn:`intuition` fails. In fact,
    :tacn:`tauto` is simply :g:`intuition fail`.

plugins/ltac/tauto.ml

@@ -256,19 +256,6 @@ let with_flags flags _ ist =
   let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
   eval_tactic_ist ist (CAst.make @@ TacArg (TacCall (CAst.make (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
 
-let warn_auto_with_star = CWarnings.create ~name:"intuition-auto-with-star" ~category:Deprecation.Version.v8_17
-    Pp.(fun () ->
-        str "\"auto with *\" was used through the default \"intuition_solver\" tactic."
-        ++ spc() ++ str "This will be replaced by just \"auto\" in the future.")
-
-let warn_auto_with_star_tac _ _ =
-  Proofview.tclBIND
-    (Proofview.tclUNIT ())
-    begin fun () ->
-      warn_auto_with_star ();
-      Proofview.tclUNIT()
-    end
-
 let val_of_id id =
   let open Geninterp in
   let id = CAst.make @@ Tactypes.IntroNaming (IntroIdentifier id) in
@@ -327,5 +314,4 @@ let () = register_tauto_tactic apply_nnpp "apply_nnpp" []
 let () = register_tauto_tactic reduction_not_iff "reduction_not_iff" []
 let () = register_tauto_tactic (with_flags tauto_uniform_unit_flags) "with_uniform_flags" ["f"]
 let () = register_tauto_tactic (with_flags tauto_power_flags) "with_power_flags" ["f"]
-let () = register_tauto_tactic warn_auto_with_star_tac "warn_auto_with_star" []
 let () = register_tauto_tactic find_cut "find_cut" ["k"]

theories/Init/Tauto.v

@@ -105,9 +105,7 @@ Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flag
 Ltac tauto := with_uniform_flags ltac:(fun flags => tauto_gen flags).
 Ltac dtauto := with_power_flags ltac:(fun flags => tauto_gen flags).
 
-Ltac intuition_solver :=
-  first [solve [auto]
-        | tryif solve [auto with *] then warn_auto_with_star else idtac].
+Ltac intuition_solver := auto.
 
 Local Ltac intuition_then tac := with_uniform_flags ltac:(fun flags => intuition_gen flags tac).
 Ltac intuition := intuition_then ltac:(idtac;intuition_solver).