diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-06-15 19:00:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | b0c84990af22e52e659bd2469af95ad2f39a047e (patch) | |
| tree | b77ca1cebe3c7fc549a172d8c8a010e9d52ac151 /tactics/class_tactics.mli | |
| parent | d041793ec3cad022ae54e4072f4f4b52b3cd1970 (diff) | |
Typeclasses:rename solve_instantiation* & use Hook
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 2fb0bbb04..8db264ad9 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -31,7 +31,7 @@ val not_evar : constr -> unit Proofview.tactic val is_ground : constr -> tactic val autoapply : constr -> Hints.hint_db_name -> tactic - + module Search : sig val eauto_tac : ?st:Names.transparent_state -> @@ -41,7 +41,7 @@ module Search : sig depth:Int.t option -> (** Bounded or unbounded search *) dep:bool -> - (** Should the tactic be made backtracking on the initial goals, + (** Should the tactic be made backtracking on the initial goals, whatever their internal dependencies are. *) Hints.hint_db list -> (** The list of hint databases to use *) |