package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
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 Names.evaluable_global_reference
  6. | Extern of Genarg.glob_generic_argument
type hint
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
type !'a with_metadata = private {
  1. pri : int;
  2. poly : Decl_kinds.polymorphic;
  3. pat : Pattern.constr_pattern option;
  4. name : hints_path_atom;
  5. db : hint_db_name option;
  6. secvars : Names.Id.Pred.t;
  7. code : 'a;
}
type full_hint = hint with_metadata
type search_entry
type hint_entry
type reference_or_constr =
  1. | HintsReference of Libnames.qualid
  2. | HintsConstr of Constrexpr.constr_expr
type hint_mode =
  1. | ModeInput
  2. | ModeNoHeadEvar
  3. | ModeOutput
type !'a hints_transparency_target =
  1. | HintsVariables
  2. | HintsConstants
  3. | HintsReferences of 'a list
type hints_expr =
  1. | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
  2. | HintsResolveIFF of bool * Libnames.qualid list * int option
  3. | HintsImmediate of reference_or_constr list
  4. | HintsUnfold of Libnames.qualid list
  5. | HintsTransparency of Libnames.qualid hints_transparency_target * bool
  6. | HintsMode of Libnames.qualid * hint_mode list
  7. | HintsConstructors of Libnames.qualid list
  8. | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
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
module Hint_db : sig ... end
type hint_db = Hint_db.t
type hnf = bool
type hint_term =
  1. | IsGlobRef of Names.GlobRef.t
  2. | IsConstr of EConstr.constr * Univ.ContextSet.t
type hints_entry =
  1. | HintsResolveEntry of (Typeclasses.hint_info * Decl_kinds.polymorphic * hnf * hints_path_atom * hint_term) list
  2. | HintsImmediateEntry of (hints_path_atom * Decl_kinds.polymorphic * hint_term) list
  3. | HintsCutEntry of hints_path
  4. | HintsUnfoldEntry of Names.evaluable_global_reference list
  5. | HintsTransparencyEntry of Names.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
val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
val remove_hints : bool -> 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 : local:bool -> hint_db_name list -> hints_entry -> unit
val prepare_hint : bool -> (bool * bool) -> Environ.env -> Evd.evar_map -> (Evd.evar_map * EConstr.constr) -> hint_term
val make_exact_entry : Environ.env -> Evd.evar_map -> Typeclasses.hint_info -> Decl_kinds.polymorphic -> ?name:hints_path_atom -> (EConstr.constr * EConstr.types * Univ.ContextSet.t) -> hint_entry
val make_apply_entry : Environ.env -> Evd.evar_map -> (bool * bool * bool) -> Typeclasses.hint_info -> Decl_kinds.polymorphic -> ?name:hints_path_atom -> (EConstr.constr * EConstr.types * Univ.ContextSet.t) -> hint_entry
val make_resolves : Environ.env -> Evd.evar_map -> (bool * bool * bool) -> Typeclasses.hint_info -> Decl_kinds.polymorphic -> ?name:hints_path_atom -> hint_term -> hint_entry list
val make_resolve_hyp : Environ.env -> Evd.evar_map -> EConstr.named_declaration -> hint_entry list
val make_extern : int -> Pattern.constr_pattern option -> Genarg.glob_generic_argument -> hint_entry
val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast
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
val wrap_hint_warning_fun : Environ.env -> Evd.evar_map -> (Evd.evar_map -> 'a * Evd.evar_map) -> 'a * Evd.evar_map
val pr_searchtable : Environ.env -> Evd.evar_map -> Pp.t
val pr_applicable_hint : Proof_global.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
val pr_hint : Environ.env -> Evd.evar_map -> hint -> 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