Default intuition solver is now auto

Author: SkySkimmer

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).