diff options
-rw-r--r-- | pretyping/typeclasses.ml | 12 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 4 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 4 | ||||
-rw-r--r-- | tactics/class_tactics.mli | 4 |
4 files changed, 12 insertions, 12 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 3ff96cd72..d57eef2e1 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -46,10 +46,10 @@ let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency let (classes_transparent_state, classes_transparent_state_hook) = Hook.make () let classes_transparent_state () = Hook.get classes_transparent_state () -let solve_instantiation_problem = ref (fun _ _ _ _ -> assert false) +let get_solve_one_instance, solve_one_instance_hook = Hook.make () let resolve_one_typeclass ?(unique=get_typeclasses_unique_solutions ()) env evm t = - !solve_instantiation_problem env evm t unique + Hook.get get_solve_one_instance env evm t unique type direction = Forward | Backward @@ -539,10 +539,10 @@ let has_typeclasses filter evd = in Evar.Map.exists check (Evd.undefined_map evd) -let solve_instantiations_problem = ref (fun _ _ _ _ _ _ -> assert false) +let get_solve_all_instances, solve_all_instances_hook = Hook.make () -let solve_problem env evd filter unique split fail = - !solve_instantiations_problem env evd filter unique split fail +let solve_all_instances env evd filter unique split fail = + Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) (* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) @@ -551,4 +551,4 @@ let solve_problem env evd filter unique split fail = let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = if not (has_typeclasses filter evd) then evd - else solve_problem env evd filter unique split fail + else solve_all_instances env evd filter unique split fail diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 7bb0ef3ab..25460ef7d 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -119,8 +119,8 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> bool -> int option -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit -val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) ref -val solve_instantiation_problem : (env -> evar_map -> types -> bool -> open_constr) ref +val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t +val solve_one_instance_hook : (env -> evar_map -> types -> bool -> open_constr) Hook.t val declare_instance : int option -> bool -> global_reference -> unit diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 714e12e3d..01c9cda49 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 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 *) |