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_hnf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types
  • deprecated This is a no-op now
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
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use Tacred.pf_reduce_to_atomic_ind
  • deprecated Use the version in Tacmach.New
  • deprecated Use Tacred.unfoldn
  • deprecated Use Environ.constant_value_in
val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
  • deprecated Use the version in Tacmach.New
val pr_gls : Goal.goal Evd.sigma -> Pp.t

Pretty-printing functions (debug only).

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