package coq

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

Module Tacmach.OldSource

  • deprecated Use the new engine
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 : Evar.t Evd.sigma -> int -> Names.Id.t
Sourceval pf_ids_of_hyps : Evar.t Evd.sigma -> Names.Id.t list
  • deprecated This is a no-op now
Sourceval pf_get_hyp_typ : Evar.t Evd.sigma -> Names.Id.t -> EConstr.types
Sourceval pf_get_new_id : Names.Id.t -> Evar.t Evd.sigma -> Names.Id.t
Sourceval pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Evar.t Evd.sigma -> 'a
Sourceval pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> Evar.t Evd.sigma -> 'a -> Evar.t 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
Sourceval pf_conv_x : Evar.t Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
  • deprecated Use the version in Tacmach.New
Sourceval pr_gls : Evar.t Evd.sigma -> Pp.t

Pretty-printing functions (debug only).

OCaml

Innovation. Community. Security.