package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
  • deprecated Use the new engine
type tactic = Proofview.V82.tac
val sig_it : 'a Evd.sigma -> 'a
val project : Evar.t Evd.sigma -> Evd.evar_map
val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma
val pf_concl : Evar.t Evd.sigma -> EConstr.types
val pf_env : Evar.t Evd.sigma -> Environ.env
val pf_nth_hyp_id : Evar.t Evd.sigma -> int -> Names.Id.t
val pf_ids_of_hyps : Evar.t Evd.sigma -> Names.Id.t list
val pf_hnf_type_of : Evar.t Evd.sigma -> EConstr.constr -> EConstr.types
  • deprecated This is a no-op now
val pf_get_hyp_typ : Evar.t Evd.sigma -> Names.Id.t -> EConstr.types
val pf_get_new_id : Names.Id.t -> Evar.t Evd.sigma -> Names.Id.t
val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Evar.t Evd.sigma -> 'a
val 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
val pf_hnf_constr : Evar.t Evd.sigma -> EConstr.constr -> EConstr.constr
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
val pf_nf_betaiota : Evar.t Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_reduce_to_quantified_ind : Evar.t Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types
  • deprecated Use Tacred.pf_reduce_to_atomic_ind
  • deprecated Use the version in Tacmach.New
  • deprecated Use Tacred.unfoldn
val pf_const_value : Evar.t Evd.sigma -> Constr.pconstant -> EConstr.constr
  • deprecated Use Environ.constant_value_in
val pf_conv_x : Evar.t Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
  • deprecated Use the version in Tacmach.New
val pr_gls : Evar.t Evd.sigma -> Pp.t

Pretty-printing functions (debug only).