diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-27 19:37:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 855143c550cad6694f77a782d1056b07f8197bd3 (patch) | |
| tree | 45ba61851044e31d4b3a8e2d1a0132e985656db9 /tactics/class_tactics.mli | |
| parent | 9e6696d67c7613b665799f7fe7f1a35cf4daf4b3 (diff) | |
bteauto: a Proofview.tactic for multiple goals
Add an option to force backtracking at toplevel, which
is used by default when calling typeclasses eauto on a set of goals.
They might be depended on by other subgoals, so the tactic should
be backtracking by default, a once can make it not backtrack.
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index e9d915de1..48abba1aa 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -23,7 +23,7 @@ val get_typeclasses_depth : unit -> int option val progress_evars : unit Proofview.tactic -> unit Proofview.tactic val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> - Hints.hint_db_name list -> tactic + Hints.hint_db_name list -> unit Proofview.tactic val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic @@ -49,6 +49,8 @@ val make_autogoal' : ?st:Names.transparent_state -> Hints.hints_path -> int -> ([ `NF ], 'c) Proofview.Goal.t -> newautoinfo val new_eauto_tac : ?st:Names.transparent_state -> - bool -> ?limit:Int.t -> - Hints.hint_db list -> unit Proofview.tactic + bool -> ?limit:Int.t -> + bool -> (* Should the tactic be made backtracking, whatever the dependencies + betwwen initial goals are *) + Hints.hint_db list -> unit Proofview.tactic |