diff options
| author | Matthieu Sozeau | 2016-06-15 19:00:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | b0c84990af22e52e659bd2469af95ad2f39a047e (patch) | |
| tree | b77ca1cebe3c7fc549a172d8c8a010e9d52ac151 /tactics | |
| parent | d041793ec3cad022ae54e4072f4f4b52b3cd1970 (diff) | |
Typeclasses:rename solve_instantiation* & use Hook
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 714e12e3d7..01c9cda49b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1446,7 +1446,7 @@ let solve_inst env evd filter unique split fail = unique env evd filter split fail let _ = - Typeclasses.solve_instantiations_problem := solve_inst + Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in @@ -1472,7 +1472,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = evd, term let _ = - Typeclasses.solve_instantiation_problem := + Hook.set Typeclasses.solve_one_instance_hook (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) (** Take the head of the arity of a constr. diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 2fb0bbb04a..8db264ad95 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 *) |