diff options
| -rw-r--r-- | doc/changelog/04-tactics/13381-bfs_eauto.rst | 6 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 1 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 1 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 29 | ||||
| -rw-r--r-- | tactics/eauto.mli | 1 |
5 files changed, 35 insertions, 3 deletions
diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst new file mode 100644 index 0000000000..a2c5e44340 --- /dev/null +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -0,0 +1,6 @@ +- **Deprecated:** + "eauto @int_or_var @int_or_var" in favor of new "bfs eauto". + Also deprecated 2-integer option for "debug eauto" and "info_eauto"; + replacement TBD. + (`#13381 <https://github.com/coq/coq/pull/13381>`_, + by Jim Fehrle). diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index a787d769fb..033ece04de 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1623,6 +1623,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "dfs" "eauto" OPT int_or_var auto_using hintbases +| "bfs" "eauto" OPT int_or_var auto_using hintbases | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" hyp | "autounfold_one" hintbases diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index c697043f27..34c3665d1d 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1746,6 +1746,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases +| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases | "autounfold" OPT hintbases OPT clause_dft_concl | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 44472a1995..6e1721fb53 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 diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 5fb038a767..f40bbc813e 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -30,4 +30,5 @@ val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic +val make_depth : int option -> int val make_dimension : int option -> int option -> bool * int |