diff options
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 70 |
1 files changed, 36 insertions, 34 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 1be3e0c5..1811150c 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -1,20 +1,22 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Pp open Util open Names -open Term +open EConstr open Environ open Globnames open Decl_kinds open Evd open Misctypes +open Tactypes open Clenv open Pattern open Vernacexpr @@ -23,9 +25,11 @@ open Vernacexpr exception Bound -val decompose_app_bound : constr -> global_reference * constr array +val decompose_app_bound : evar_map -> constr -> global_reference * constr array -val secvars_of_hyps : Context.Named.t -> Id.Pred.t +type debug = Debug | Info | Off + +val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t val empty_hint_info : 'a hint_info_gen @@ -40,7 +44,7 @@ type 'a hint_ast = | Extern of Genarg.glob_generic_argument (* Hint Extern *) type hint -type raw_hint = constr * types * Univ.universe_context_set +type raw_hint = constr * types * Univ.ContextSet.t type 'a hints_path_atom_gen = | PathHints of 'a list @@ -82,10 +86,10 @@ type hints_path = global_reference hints_path_gen val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool val path_derivate : hints_path -> hints_path_atom -> hints_path -val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds -val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds -val pp_hints_path : hints_path -> Pp.std_ppcmds -val pp_hint_mode : hint_mode -> Pp.std_ppcmds +val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t +val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t +val pp_hints_path : hints_path -> Pp.t +val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen val glob_hints_path : @@ -107,16 +111,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 @@ -144,7 +148,7 @@ type hint_info = (patvar list * constr_pattern) hint_info_gen type hint_term = | IsGlobRef of global_reference - | IsConstr of constr * Univ.universe_context_set + | IsConstr of constr * Univ.ContextSet.t type hints_entry = | HintsResolveEntry of @@ -154,7 +158,7 @@ type hints_entry = | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list - | HintsExternEntry of hint_info * Tacexpr.glob_tactic_expr + | HintsExternEntry of hint_info * Genarg.glob_generic_argument val searchtable_map : hint_db_name -> hint_db @@ -179,7 +183,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 info (c, ctyp, ctx)]. [c] is the term given as an exact proof to solve the goal; @@ -191,7 +195,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> *) val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom -> - (constr * types * Univ.universe_context_set) -> hint_entry + (constr * types * Univ.ContextSet.t) -> hint_entry (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))]. [eapply] is true if this hint will be used only with EApply; @@ -209,7 +213,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint val make_apply_entry : env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom -> - (constr * types * Univ.universe_context_set) -> hint_entry + (constr * types * Univ.ContextSet.t) -> hint_entry (** A constr which is Hint'ed will be: - (1) used as an Exact, if it does not start with a product @@ -228,12 +232,12 @@ val make_resolves : If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : - env -> evar_map -> Context.Named.Declaration.t -> hint_entry list + env -> evar_map -> named_declaration -> hint_entry list (** [make_extern pri pattern tactic_expr] *) val make_extern : - int -> constr_pattern option -> Tacexpr.glob_tactic_expr + int -> constr_pattern option -> Genarg.glob_generic_argument -> hint_entry val run_hint : hint -> @@ -243,14 +247,11 @@ val run_hint : hint -> written code. *) val repr_hint : hint -> (raw_hint * clausenv) hint_ast -val extern_intern_tac : - (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t - (** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) -val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> Tacexpr.delayed_open_constr list -> hint_db +val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> delayed_open_constr list -> hint_db val make_db_list : hint_db_name list -> hint_db list @@ -261,14 +262,15 @@ val rewrite_db : hint_db_name (** Printing hints *) -val pr_searchtable : unit -> std_ppcmds -val pr_applicable_hint : unit -> std_ppcmds -val pr_hint_ref : global_reference -> std_ppcmds -val pr_hint_db_by_name : hint_db_name -> std_ppcmds -val pr_hint_db : Hint_db.t -> std_ppcmds -val pr_hint : hint -> Pp.std_ppcmds +val pr_searchtable : env -> evar_map -> Pp.t +val pr_applicable_hint : unit -> Pp.t +val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t +val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t +val pr_hint_db : Hint_db.t -> Pp.t +[@@ocaml.deprecated "please used pr_hint_db_env"] +val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) - val add_hints_init : (unit -> unit) -> unit |