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) -> 'b Proofview.Goal.t -> 'a
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
val project : 'a Proofview.Goal.t -> Evd.evar_map
val pf_env : 'a Proofview.Goal.t -> Environ.env
val pf_concl : 'a Proofview.Goal.t -> EConstr.types
val pf_unsafe_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
val pf_get_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
val pf_conv_x : 'a Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.identifier list
val pf_hyps_types : 'a Proofview.Goal.t -> (Names.identifier * EConstr.types) list
val pf_get_hyp_typ : Names.identifier -> 'a Proofview.Goal.t -> EConstr.types
val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> EConstr.types
val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types
val pf_hnf_constr : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
val pf_hnf_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types
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