diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-20 03:40:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | b91d322b646edf753ca9f3659563e4d6c525d3f6 (patch) | |
| tree | 519fb31febe2cc6e7be6e9ac6839d6f424d3b2d4 /tactics/class_tactics.mli | |
| parent | 2c07b6d95c7b8fd754cdf9dd767dda989723125a (diff) | |
Typeclasses: refine the eauto tactic
- Treat shelved dependent subgoals that might not be
resolved after some proof search correctly by restarting
their resolution as soon as possible (if they are
typeclasses in only_classes mode).
- Treat dependencies between goals better, avoiding
backtracking more often when dependencies allow.
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 6b4ff8b5e..e9d915de1 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -36,6 +36,7 @@ val autoapply : constr -> Hints.hint_db_name -> tactic type newautoinfo = { search_depth : int list; last_tac : Pp.std_ppcmds Lazy.t; + search_dep : bool; search_cut : Hints.hints_path; search_hints : Hints.Hint_db.t } @@ -43,8 +44,8 @@ val new_hints_tac : bool -> Hints.hint_db list -> newautoinfo -> (newautoinfo -> unit Proofview.tactic) -> unit Proofview.tactic -val make_autogoal' : ?st:Names.transparent_state -> - bool -> +val make_autogoal' : ?st:Names.transparent_state -> + bool -> bool -> Hints.hints_path -> int -> ([ `NF ], 'c) Proofview.Goal.t -> newautoinfo val new_eauto_tac : ?st:Names.transparent_state -> |