Module Tacmach

Operations for handling terms under a local typing context.

type tactic = Proofview.V82.tac
val sig_it : 'a Evd.sigma -> 'a
val project : Goal.goal Evd.sigma -> Evd.evar_map
val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma
val pf_concl : Goal.goal Evd.sigma -> EConstr.types
val pf_env : Goal.goal Evd.sigma -> Environ.env
val pf_hyps : Goal.goal Evd.sigma -> EConstr.named_context
val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t Context.binder_annot * EConstr.types) list
val pf_nth_hyp_id : Goal.goal Evd.sigma -> int -> Names.Id.t
val pf_last_hyp : Goal.goal Evd.sigma -> EConstr.named_declaration
val pf_ids_of_hyps : Goal.goal Evd.sigma -> Names.Id.t list
val pf_unsafe_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types
val pf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Evd.evar_map * EConstr.types
val pf_hnf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types
val pf_get_hyp : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.named_declaration
val pf_get_hyp_typ : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.types
val pf_get_new_id : Names.Id.t -> Goal.goal Evd.sigma -> Names.Id.t
val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Goal.goal Evd.sigma -> 'a
val pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> Goal.goal Evd.sigma -> 'a -> Goal.goal Evd.sigma * 'b
val pf_reduce : (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) -> Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_e_reduce : (Environ.env -> Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr) -> Goal.goal Evd.sigma -> EConstr.constr -> Evd.evar_map * EConstr.constr
val pf_whd_all : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_hnf_constr : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_nf : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_nf_betaiota : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_reduce_to_quantified_ind : Goal.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types
val pf_reduce_to_atomic_ind : Goal.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types
val pf_compute : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_unfoldn : (Locus.occurrences * Names.evaluable_global_reference) list -> Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr
val pf_const_value : Goal.goal Evd.sigma -> Constr.pconstant -> EConstr.constr
val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
val pr_gls : Goal.goal Evd.sigma -> Pp.t
Pretty-printing functions (debug only).
module New : sig ... end

Variants of Tacmach functions built with the new proof engine