package coq-core

  1. Overview
  2. Docs
package coq-core
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.

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