package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TacmachSource

Operations for handling terms under a local typing context.

Variants of Tacmach functions built with the new proof engine

Sourceval pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Proofview.Goal.t -> 'a

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.

Sourceval pf_conv_x : Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
Sourceval pf_get_new_id : Names.Id.t -> Proofview.Goal.t -> Names.Id.t
Sourceval pf_ids_of_hyps : Proofview.Goal.t -> Names.Id.t list
Sourceval pf_ids_set_of_hyps : Proofview.Goal.t -> Names.Id.Set.t
Sourceval pf_hyps_types : Proofview.Goal.t -> (Names.Id.t * EConstr.types) list
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