package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (6)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad

doc/rocq-runtime.proofs/Tacmach/index.html

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
  • deprecated (9.2) Use Proofview.Goal.{env, sigma}
  • deprecated (9.2) Use Proofview.Goal.sigma
  • deprecated (9.2) Use Proofview.Goal.env
  • deprecated (9.2) Use Proofview.Goal.concl

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)

  • deprecated (9.2) Use Retyping.get_type_of

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

  • deprecated (9.2) Use Typing.type_of
Sourceval pf_conv_x : Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
  • deprecated (9.2) Use Reductionops.is_conv
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
  • deprecated (9.2) Use EConstr.named_context
  • deprecated (9.2) Use EConstr.named_context
  • deprecated (9.2) Use Reductionops.nf_evar
  • deprecated (9.2) Use Tacred.hnf_constr
  • deprecated (9.2) Use Reductionops.whd_all and Retyping.get_type_of
  • deprecated (9.2) Use Tacred.pf_compute
  • deprecated (9.2) Use Tacred.whd_compute
  • deprecated (9.2) Use Reductionops.nf_evar
  • deprecated (9.2) Use Printer.pr_evar