Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"

Reviewed-by: Zimmi48

1 files changed, 26 insertions, 3 deletions

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 15861d49be..7e8400910c 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -116,12 +116,25 @@ END
 
 let make_depth n = snd (Eauto.make_dimension n None)
 
+(* deprecated in 8.13; the second int_or_var will be removed *)
+let deprecated_eauto_bfs =
+  CWarnings.create
+    ~name:"eauto_bfs" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [eauto @int_or_var @int_or_var] is deprecated. Use [bfs eauto] instead.")
+
+let deprecated_bfs tacname =
+  CWarnings.create
+    ~name:"eauto_bfs" ~category:"deprecated"
+    (fun () -> Pp.str "The syntax [" ++ Pp.str tacname ++ Pp.str "@int_or_var @int_or_var] is deprecated. No replacement yet.")
+
 }
 
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+    {
+      ( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () );
+      Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND new_eauto
@@ -135,13 +148,17 @@ END
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+    {
+      ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () );
+      Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND info_eauto
 | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+    {
+      ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () );
+      Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
 END
 
 TACTIC EXTEND dfs_eauto
@@ -150,6 +167,12 @@ TACTIC EXTEND dfs_eauto
     { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db }
 END
 
+TACTIC EXTEND bfs_eauto
+| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems)
+      hintbases(db) ] ->
+    { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db }
+END
+
 TACTIC EXTEND autounfold
 | [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl }
 END