package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Proofview.Goal.t -> 'a
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
val pf_unsafe_type_of : Proofview.Goal.t -> EConstr.constr -> EConstr.types
val pf_get_type_of : Proofview.Goal.t -> EConstr.constr -> EConstr.types
val pf_conv_x : Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
val pf_get_new_id : Names.Id.t -> Proofview.Goal.t -> Names.Id.t
val pf_ids_of_hyps : Proofview.Goal.t -> Names.Id.t list
val pf_ids_set_of_hyps : Proofview.Goal.t -> Names.Id.Set.t
val pf_hyps_types : Proofview.Goal.t -> (Names.Id.t * EConstr.types) list
val pf_get_hyp_typ : Names.Id.t -> Proofview.Goal.t -> EConstr.types
val pf_nf_concl : Proofview.Goal.t -> EConstr.types
val pf_hnf_type_of : Proofview.Goal.t -> EConstr.constr -> EConstr.types