coq 8.11.0 · OCaml Package

exception Bound

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

type debug =

| Debug
| Info
| Off

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

val empty_hint_info : 'a Typeclasses.hint_info_gen

type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen

type !'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 Names.evaluable_global_reference
| Extern of Genarg.glob_generic_argument

type hint

type raw_hint = EConstr.constr * EConstr.types * Univ.ContextSet.t

type !'a hints_path_atom_gen =

| PathHints of 'a list
| PathAny

type hints_path_atom = Names.GlobRef.t hints_path_atom_gen

type hint_db_name = string

type !'a with_metadata = private {

pri : int;
poly : bool;
pat : Pattern.constr_pattern option;
name : hints_path_atom;
db : string option;
secvars : Names.Id.Pred.t;
code : 'a;

}

type full_hint = hint with_metadata

type search_entry

type hint_entry

type reference_or_constr =

| HintsReference of Libnames.qualid
| HintsConstr of Constrexpr.constr_expr

type hint_mode =

| ModeInput
| ModeNoHeadEvar
| ModeOutput

type !'a hints_transparency_target =

| HintsVariables
| HintsConstants
| HintsReferences of 'a list

type hints_expr =

| HintsResolve of (hint_info_expr * bool * reference_or_constr) list
| HintsResolveIFF of bool * Libnames.qualid list * int option
| HintsImmediate of reference_or_constr list
| HintsUnfold of Libnames.qualid list
| HintsTransparency of Libnames.qualid hints_transparency_target * bool
| HintsMode of Libnames.qualid * hint_mode list
| HintsConstructors of Libnames.qualid list
| HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument

type !'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

type pre_hints_path = Libnames.qualid hints_path_gen

type hints_path = Names.GlobRef.t 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

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

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

module Hint_db : sig ... end

type hint_db = Hint_db.t

type hnf = bool

type hint_term =

| IsGlobRef of Names.GlobRef.t
| IsConstr of EConstr.constr * Univ.ContextSet.t

type hints_entry =

| HintsResolveEntry of (Typeclasses.hint_info * bool * hnf * hints_path_atom * hint_term) list
| HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of Names.evaluable_global_reference list
| HintsTransparencyEntry of Names.evaluable_global_reference hints_transparency_target * bool
| HintsModeEntry of Names.GlobRef.t * hint_mode list
| 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 interp_hints : poly:bool -> hints_expr -> hints_entry

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 ->
  poly:bool ->
  ?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 ->
  poly:bool ->
  ?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 ->
  poly:bool ->
  ?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 run_hint : 
  hint ->
  ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) ->
  'r Proofview.tactic

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

package coq