package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type tactic = Proofview.V82.tac
val sig_it : 'a Evd.sigma -> 'a
val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma
val pf_nth_hyp_id : Goal.goal Evd.sigma -> int -> Names.Id.t
val pf_ids_of_hyps : Goal.goal Evd.sigma -> Names.Id.t list
val pf_unsafe_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types
  • deprecated Use [type_of] or retyping according to your needs.
val pf_hnf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types
  • deprecated This is a no-op now
val pf_get_hyp_typ : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.types
val pf_get_new_id : Names.Id.t -> Goal.goal Evd.sigma -> Names.Id.t
val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Goal.goal Evd.sigma -> 'a
val 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
val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
  • deprecated Use the version in Tacmach.New
val pr_gls : Goal.goal Evd.sigma -> Pp.t
module New : sig ... end