diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-19 02:45:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:59 +0100 |
| commit | 34e86e839be251717db96f1f5969d7724ab43097 (patch) | |
| tree | b62c2f97c7277250796b7f9b3783b95590ea98ab /tactics/hints.mli | |
| parent | 7b43de20a4acd7c9da290f038d9a16fe67eccd59 (diff) | |
Hints API using EConstr.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index c0eb2c3b8..344827e03 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -10,6 +10,7 @@ open Pp open Util open Names open Term +open EConstr open Environ open Globnames open Decl_kinds @@ -99,16 +100,16 @@ module Hint_db : (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) - val map_existential : secvars:Id.Pred.t -> + val map_existential : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list + val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) - val map_auto : secvars:Id.Pred.t -> + val map_auto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list val add_one : env -> evar_map -> hint_entry -> t -> t @@ -170,7 +171,7 @@ val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> (bool * bool) (* polymorphic or monomorphic, local or global *) -> - env -> evar_map -> open_constr -> hint_term + env -> evar_map -> evar_map * constr -> hint_term (** [make_exact_entry pri (c, ctyp, ctx, secvars)]. [c] is the term given as an exact proof to solve the goal; |