package coq

  1. Overview
  2. Docs
package coq
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.

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