package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

Variants of Tacmach functions built with the new proof engine

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

FIXME: encapsulate the level in an existential type.

val pf_unsafe_type_of : Proofview.Goal.t -> EConstr.constr -> EConstr.types

WRONG: To be avoided at all costs, it typechecks the term entirely but forgets the universe constraints necessary to retypecheck it

  • deprecated Use [type_of] or retyping according to your needs.
val pf_get_type_of : Proofview.Goal.t -> EConstr.constr -> EConstr.types

This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved)

This function entirely type-checks the term and computes its type and the implied universe constraints.

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