diff options
| author | coqbot-app[bot] | 2020-11-16 12:11:15 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 12:11:15 +0000 |
| commit | c3e7b6bec355e69f58a4adf093a1454a57dbac6a (patch) | |
| tree | 3d84c8d791474c6b5b87775d3725bb45b2004ebb /tactics | |
| parent | 8a1e9bb57462614028eb1b3905fb1df1cdf3a871 (diff) | |
| parent | 7b8da8cb0327f3bc5c008b76a29cf4e05585e2ae (diff) | |
Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"
Reviewed-by: Zimmi48
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |