Module `Tacmach`Source

Operations for handling terms under a local typing context.

Sourcetype tactic = Evar.t Evd.sigma -> Evar.t list Evd.sigma

Sourceval sig_it : 'a Evd.sigma -> 'a

Sourceval project : Goal.goal Evd.sigma -> Evd.evar_map

Sourceval re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma

Sourceval pf_concl : Goal.goal Evd.sigma -> EConstr.types

Sourceval pf_env : Goal.goal Evd.sigma -> Environ.env

Sourceval pf_hyps : Goal.goal Evd.sigma -> EConstr.named_context

Source

val pf_hyps_types : 
  Goal.goal Evd.sigma ->
  (Names.Id.t Context.binder_annot * EConstr.types) list

Sourceval pf_nth_hyp_id : Goal.goal Evd.sigma -> int -> Names.Id.t

Sourceval pf_last_hyp : Goal.goal Evd.sigma -> EConstr.named_declaration

Sourceval pf_ids_of_hyps : Goal.goal Evd.sigma -> Names.Id.t list

Sourceval pf_unsafe_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types

deprecated Use [type_of] or retyping according to your needs.

Source

val pf_type_of : 
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  Evd.evar_map * EConstr.types

Sourceval pf_hnf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types

deprecated This is a no-op now

Sourceval pf_get_hyp : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.named_declaration

Sourceval pf_get_hyp_typ : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.types

Sourceval pf_get_new_id : Names.Id.t -> Goal.goal Evd.sigma -> Names.Id.t

Sourceval pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Goal.goal Evd.sigma -> 'a

Source

val pf_eapply : 
  (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) ->
  Goal.goal Evd.sigma ->
  'a ->
  Goal.goal Evd.sigma * 'b

Source

val pf_reduce : 
  (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) ->
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  EConstr.constr

deprecated Use the version in Tacmach.New

Source

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

deprecated Use the version in Tacmach.New

Sourceval pf_whd_all : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

deprecated Use the version in Tacmach.New

Sourceval pf_hnf_constr : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

deprecated Use the version in Tacmach.New

Sourceval pf_nf : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

deprecated Use the version in Tacmach.New

Sourceval pf_nf_betaiota : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

Source

val pf_reduce_to_quantified_ind : 
  Goal.goal Evd.sigma ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.types

Source

val pf_reduce_to_atomic_ind : 
  Goal.goal Evd.sigma ->
  EConstr.types ->
  (Names.inductive * EConstr.EInstance.t) * EConstr.types

deprecated Use Tacred.pf_reduce_to_atomic_ind

Sourceval pf_compute : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr

deprecated Use the version in Tacmach.New

Source

val pf_unfoldn : 
  (Locus.occurrences * Tacred.evaluable_global_reference) list ->
  Goal.goal Evd.sigma ->
  EConstr.constr ->
  EConstr.constr

deprecated Use Tacred.unfoldn

Sourceval pf_const_value : Goal.goal Evd.sigma -> Constr.pconstant -> EConstr.constr

deprecated Use Environ.constant_value_in

Sourceval pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool

deprecated Use the version in Tacmach.New

Sourceval pr_gls : Goal.goal Evd.sigma -> Pp.t

Pretty-printing functions (debug only).

Sourcemodule New : sig ... end

Variants of Tacmach functions built with the new proof engine

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.proofs/Tacmach/index.html

Module `Tacmach`Source

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.proofs/Tacmach/index.html

Module TacmachSource

Module `Tacmach`Source