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