package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
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
  • 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