diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 00:35:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:23 +0100 |
| commit | 67507df457be05ee5b651a423031a8cd584934ef (patch) | |
| tree | 70aa18b06c278818b8329070429a39152218c104 /pretyping/typeclasses.mli | |
| parent | e71f6d24465ea7812e9b893ed8e0deb2a44ce4f8 (diff) | |
Class_tactics API using EConstr.
Diffstat (limited to 'pretyping/typeclasses.mli')
| -rw-r--r-- | pretyping/typeclasses.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index ec36c57e0..e95aba695 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -103,7 +103,7 @@ val is_class_type : evar_map -> EConstr.types -> bool val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map -val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> open_constr +val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -120,7 +120,7 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> val remove_instance_hint : global_reference -> unit 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 -> EConstr.types -> bool -> open_constr) Hook.t +val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t val declare_instance : int option -> bool -> global_reference -> unit |