package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac_plugin.TacinterpSource

Sourceval ltac_trace_info : Tacexpr.ltac_stack Exninfo.t
Sourcemodule Value : sig ... end
Sourcetype value = Value.t

Values for interpretation

Sourcetype 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

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

Sourceval set_debug : Tactic_debug.debug_info -> unit

Sets the debugger mode

Sourceval 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 tactic expressions

Initial call for interpretation

Same as eval_tactic, but with the provided interp_sign.

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

Globalization + interpretation

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

Hides interpretation for pretty-print

Internals that can be useful for syntax extensions.

Sourceval interp_ltac_var : (value -> 'a) -> interp_sign -> (Environ.env * Evd.evar_map) option -> Names.lident -> 'a
Sourceval interp_int : interp_sign -> Names.lident -> int
Sourceval interp_int_or_var : interp_sign -> int Locus.or_var -> int
Sourceval 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