package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
General functions.
exception Bound
val decompose_app_bound : Evd.evar_map -> EConstr.constr -> Names.GlobRef.t * EConstr.constr array
type debug =
  1. | Debug
  2. | Info
  3. | Off
val secvars_of_hyps : ('c, 't) Context.Named.pt -> Names.Id.Pred.t
val empty_hint_info : 'a Typeclasses.hint_info_gen
val hint_cat : Libobject.category

Pre-created hint databases

type 'a hint_ast =
  1. | Res_pf of 'a
  2. | ERes_pf of 'a
  3. | Give_exact of 'a
  4. | Res_pf_THEN_trivial_fail of 'a
  5. | Unfold_nth of Tacred.evaluable_global_reference
  6. | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument
type hint
val hint_as_term : hint -> Univ.ContextSet.t option * EConstr.constr
type 'a hints_path_atom_gen =
  1. | PathHints of 'a list
  2. | PathAny
type hints_path_atom = Names.GlobRef.t hints_path_atom_gen
type hint_db_name = string
module FullHint : sig ... end

The head may not be bound.

type hint_mode =
  1. | ModeInput
  2. | ModeNoHeadEvar
  3. | ModeOutput
type 'a hints_transparency_target =
  1. | HintsVariables
  2. | HintsConstants
  3. | HintsReferences of 'a list
type 'a hints_path_gen =
  1. | PathAtom of 'a hints_path_atom_gen
  2. | PathStar of 'a hints_path_gen
  3. | PathSeq of 'a hints_path_gen * 'a hints_path_gen
  4. | PathOr of 'a hints_path_gen * 'a hints_path_gen
  5. | PathEmpty
  6. | PathEpsilon
type pre_hints_path = Libnames.qualid 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.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
type mode_match =
  1. | NoMode
  2. | WithMode of hint_mode array
type 'a with_mode =
  1. | ModeMatch of mode_match * 'a
  2. | ModeMismatch
module Hint_db : sig ... end
type hint_db = Hint_db.t
type hnf = bool
type hint_term
type hints_entry =
  1. | HintsResolveEntry of (Typeclasses.hint_info * hnf * hints_path_atom * hint_term) list
  2. | HintsImmediateEntry of (hints_path_atom * hint_term) list
  3. | HintsCutEntry of hints_path
  4. | HintsUnfoldEntry of Tacred.evaluable_global_reference list
  5. | HintsTransparencyEntry of Tacred.evaluable_global_reference hints_transparency_target * bool
  6. | HintsModeEntry of Names.GlobRef.t * hint_mode list
  7. | HintsExternEntry of Typeclasses.hint_info * Genarg.glob_generic_argument
val searchtable_map : hint_db_name -> hint_db
val searchtable_add : (hint_db_name * hint_db) -> unit
type hint_locality =
  1. | Local
  2. | Export
  3. | SuperGlobal
val 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.

val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
val remove_hints : locality:hint_locality -> hint_db_name list -> Names.GlobRef.t list -> unit
val current_db_names : unit -> Util.String.Set.t
val current_pure_db : unit -> hint_db list
val add_hints : locality:hint_locality -> hint_db_name list -> hints_entry -> unit
val hint_globref : Names.GlobRef.t -> hint_term
val 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.

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.

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

val make_local_hint_db : Environ.env -> Evd.evar_map -> ?ts:TransparentState.t -> bool -> Tactypes.delayed_open_constr list -> hint_db
val make_db_list : hint_db_name list -> hint_db list
val 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.

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

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

Printing hints

val pr_searchtable : Environ.env -> Evd.evar_map -> Pp.t
val pr_applicable_hint : Proof.t -> Pp.t
val pr_hint_ref : Environ.env -> Evd.evar_map -> Names.GlobRef.t -> Pp.t
val pr_hint_db_by_name : Environ.env -> Evd.evar_map -> hint_db_name -> Pp.t
val pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct