Module `Hints`Source

General functions.

Sourceexception Bound

val decompose_app_bound : 
  Evd.evar_map ->
  EConstr.constr ->
  Names.GlobRef.t * EConstr.constr array

Sourcetype debug =

| Debug
| Info
| Off

Sourceval secvars_of_hyps : ('c, 't) Context.Named.pt -> Names.Id.Pred.t

Sourceval empty_hint_info : 'a Typeclasses.hint_info_gen

Sourceval hint_cat : Libobject.category

Pre-created hint databases

Sourcetype 'a hint_ast =

| Res_pf of 'a
| ERes_pf of 'a
| Give_exact of 'a
| Res_pf_THEN_trivial_fail of 'a
| Unfold_nth of Tacred.evaluable_global_reference
| Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument

Sourcetype hint

Sourceval hint_as_term : hint -> Univ.ContextSet.t option * EConstr.constr

Sourcetype 'a hints_path_atom_gen =

| PathHints of 'a list
| PathAny

Sourcetype hints_path_atom = Names.GlobRef.t hints_path_atom_gen

Sourcetype hint_db_name = string

Sourcemodule FullHint : sig ... end

The head may not be bound.

Sourcetype hint_mode =

| ModeInput
| ModeNoHeadEvar
| ModeOutput

Sourcetype 'a hints_transparency_target =

| HintsVariables
| HintsConstants
| HintsReferences of 'a list

Sourcetype 'a hints_path_gen =

| PathAtom of 'a hints_path_atom_gen
| PathStar of 'a hints_path_gen
| PathSeq of 'a hints_path_gen * 'a hints_path_gen
| PathOr of 'a hints_path_gen * 'a hints_path_gen
| PathEmpty
| PathEpsilon

Sourcetype pre_hints_path = Libnames.qualid hints_path_gen

Sourcetype hints_path = Names.GlobRef.t hints_path_gen

Sourceval normalize_path : hints_path -> hints_path

Sourceval path_matches : hints_path -> hints_path_atom list -> bool

Sourceval path_derivate : hints_path -> hints_path_atom -> hints_path

Sourceval pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t

Sourceval pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t

Sourceval pp_hints_path : hints_path -> Pp.t

Sourceval pp_hint_mode : hint_mode -> Pp.t

Source

val glob_hints_path_atom : 
  Libnames.qualid hints_path_atom_gen ->
  Names.GlobRef.t hints_path_atom_gen

Source

val glob_hints_path : 
  Libnames.qualid hints_path_gen ->
  Names.GlobRef.t hints_path_gen

Sourcetype mode_match =

| NoMode
| WithMode of hint_mode array

Sourcetype 'a with_mode =

| ModeMatch of mode_match * 'a
| ModeMismatch

Sourcemodule Hint_db : sig ... end

Sourcetype hint_db = Hint_db.t

Sourcetype hnf = bool

Sourcetype hint_term

Sourcetype hints_entry =

| HintsResolveEntry of (Typeclasses.hint_info * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of Tacred.evaluable_global_reference list
| HintsTransparencyEntry of Tacred.evaluable_global_reference hints_transparency_target * bool
| HintsModeEntry of Names.GlobRef.t * hint_mode list
| HintsExternEntry of Typeclasses.hint_info * Genarg.glob_generic_argument

Sourceval searchtable_map : hint_db_name -> hint_db

Sourceval searchtable_add : (hint_db_name * hint_db) -> unit

Sourcetype hint_locality =

| Local
| Export
| SuperGlobal

Sourceval default_hint_locality : unit -> hint_locality

Warns

create_hint_db local name st use_dn. st is a transparency state for unification using this db use_dn switches the use of the discrimination net for all hints and patterns.

Sourceval create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit

Source

val remove_hints : 
  locality:hint_locality ->
  hint_db_name list ->
  Names.GlobRef.t list ->
  unit

Sourceval current_db_names : unit -> Util.String.Set.t

Sourceval current_pure_db : unit -> hint_db list

Source

val add_hints : 
  locality:hint_locality ->
  hint_db_name list ->
  hints_entry ->
  unit

Sourceval hint_globref : Names.GlobRef.t -> hint_term

Sourceval hint_constr : (EConstr.constr * Univ.ContextSet.t option) -> hint_term

A constr which is Hint'ed will be:

(1) used as an Exact, if it does not start with a product
(2) used as an Apply, if its HNF starts with a product, and has no missing arguments.
(3) used as an EApply, if its HNF starts with a product, and has missing arguments.

Source

val push_resolves : 
  Environ.env ->
  Evd.evar_map ->
  Names.GlobRef.t ->
  Hint_db.t ->
  Hint_db.t

push_resolve_hyp hname htyp db. used to add an hypothesis to the local hint database; Never raises a user exception; If the hyp cannot be used as a Hint, it is not added.

Source

val push_resolve_hyp : 
  Environ.env ->
  Evd.evar_map ->
  Names.Id.t ->
  Hint_db.t ->
  Hint_db.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

Source

val make_local_hint_db : 
  Environ.env ->
  Evd.evar_map ->
  ?ts:TransparentState.t ->
  bool ->
  Tactypes.delayed_open_constr list ->
  hint_db

Sourceval make_db_list : hint_db_name list -> hint_db list

Sourceval wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic

Use around toplevel calls to hint-using tactics, to enable the tracking of non-imported hints. Any tactic calling run_hint must be wrapped this way.

Source

val wrap_hint_warning_fun : 
  Environ.env ->
  Evd.evar_map ->
  (Evd.evar_map -> 'a * Evd.evar_map) ->
  'a * Evd.evar_map

Variant of the above for non-tactics

Source

val fresh_hint : 
  Environ.env ->
  Evd.evar_map ->
  hint ->
  Evd.evar_map * EConstr.constr

Source

val hint_res_pf : 
  ?with_evars:bool ->
  ?with_classes:bool ->
  ?flags:Unification.unify_flags ->
  hint ->
  unit Proofview.tactic

Printing hints

Sourceval pr_searchtable : Environ.env -> Evd.evar_map -> Pp.t

Sourceval pr_applicable_hint : Proof.t -> Pp.t

Sourceval pr_hint_ref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Pp.t

Sourceval pr_hint_db_by_name : Environ.env -> Evd.evar_map -> hint_db_name -> Pp.t

Sourceval pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.tactics/Hints/index.html

Module `Hints`Source

General functions.

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.tactics/Hints/index.html

Module HintsSource

General functions.

Module `Hints`Source