package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val ltac_trace_info : Tacexpr.ltac_stack Exninfo.t
module Value : sig ... end
type value = Value.t

Values for interpretation

type interp_sign = Geninterp.interp_sign = {
  1. lfun : value Names.Id.Map.t;
  2. poly : bool;
  3. extra : TacStore.t;
}

Signature for interpretation: val\_interp and interpretation functions

val f_avoid_ids : Names.Id.Set.t TacStore.field

Given an interpretation signature, extract all values which are coercible to a constr.

val set_debug : Tactic_debug.debug_info -> unit

Sets the debugger mode

val get_debug : unit -> Tactic_debug.debug_info

Gives the state of debug

Adds an interpretation function for extra generic arguments

Interprets any expression

Interprets an expression that evaluates to a constr

Interprets redexp arguments

Interprets redexp arguments from a raw one

Interprets tactic expressions

Initial call for interpretation

val eval_tactic : Tacexpr.glob_tactic_expr -> unit Proofview.tactic
val eval_tactic_ist : interp_sign -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic

Same as eval_tactic, but with the provided interp_sign.

val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic

Globalization + interpretation

type ltac_expr = {
  1. global : bool;
  2. ast : Tacexpr.raw_tactic_expr;
}

Hides interpretation for pretty-print

val hide_interp : ltac_expr -> ComTactic.interpretable

Internals that can be useful for syntax extensions.

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

Empty ist with debug set on the current value.