package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val ltac_trace_info : Tacexpr.ltac_trace Exninfo.t
module Value : sig ... end
type value = Value.t
module TacStore : sig ... end
type interp_sign = Geninterp.interp_sign = {
  1. lfun : value Names.Id.Map.t;
  2. poly : bool;
  3. extra : TacStore.t;
}
val f_avoid_ids : Names.Id.Set.t TacStore.field
val set_debug : Tactic_debug.debug_info -> unit
val get_debug : unit -> Tactic_debug.debug_info
val eval_tactic : Tacexpr.glob_tactic_expr -> unit Proofview.tactic
val eval_tactic_ist : interp_sign -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic
val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic
type ltac_expr = {
  1. global : bool;
  2. ast : Tacexpr.raw_tactic_expr;
}
val hide_interp : ltac_expr -> ComTactic.interpretable
val interp_ltac_var : (value -> 'a) -> interp_sign -> (Environ.env * Evd.evar_map) option -> Names.lident -> 'a
val interp_int : interp_sign -> Names.lident -> int
val interp_int_or_var : interp_sign -> int Locus.or_var -> int
val default_ist : unit -> Geninterp.interp_sign
OCaml

Innovation. Community. Security.