package coq

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TacmachSource

Operations for handling terms under a local typing context.

Sourcetype tactic = Evar.t Evd.sigma -> Evar.t list Evd.sigma
Sourceval sig_it : 'a Evd.sigma -> 'a
Sourceval re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma
Sourceval pf_nth_hyp_id : Goal.goal Evd.sigma -> int -> Names.Id.t
Sourceval pf_ids_of_hyps : Goal.goal Evd.sigma -> Names.Id.t list
  • deprecated Use [type_of] or retyping according to your needs.
  • deprecated This is a no-op now
Sourceval pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Goal.goal Evd.sigma -> 'a
Sourceval pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> Goal.goal Evd.sigma -> 'a -> Goal.goal Evd.sigma * 'b
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use Tacred.pf_reduce_to_atomic_ind
  • deprecated Use the version in Tacmach.New
  • deprecated Use Tacred.unfoldn
  • deprecated Use Environ.constant_value_in
  • deprecated Use the version in Tacmach.New

Pretty-printing functions (debug only).

Sourcemodule New : sig ... end

Variants of Tacmach functions built with the new proof engine

OCaml

Innovation. Community. Security.