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 : (Goal.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
val pf_unsafe_type_of : Proofview.Goal.t -> EConstr.constr -> EConstr.types
  • deprecated Use [type_of] or retyping according to your needs.
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
val pr_gls : Proofview.Goal.t -> Pp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct