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
val pf_hnf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types
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
val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
val pr_gls : Goal.goal Evd.sigma -> Pp.t
module New : sig ... end
OCaml

Innovation. Community. Security.