package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Tacmach.OldSource

  • deprecated Use the new engine
Sourcetype tactic = Evar.t Evd.sigma -> Evar.t list Evd.sigma
Sourceval sig_it : 'a Evd.sigma -> 'a
Sourceval re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma
Sourceval pf_nth_hyp_id : Evar.t Evd.sigma -> int -> Names.Id.t
Sourceval pf_ids_of_hyps : Evar.t Evd.sigma -> Names.Id.t list
  • deprecated This is a no-op now
Sourceval pf_get_hyp_typ : Evar.t Evd.sigma -> Names.Id.t -> EConstr.types
Sourceval pf_get_new_id : Names.Id.t -> Evar.t Evd.sigma -> Names.Id.t
Sourceval pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Evar.t Evd.sigma -> 'a
Sourceval pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> Evar.t Evd.sigma -> 'a -> Evar.t Evd.sigma * 'b
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use the version in Tacmach.New
  • deprecated Use Tacred.pf_reduce_to_atomic_ind
  • deprecated Use the version in Tacmach.New
  • deprecated Use Tacred.unfoldn
  • deprecated Use Environ.constant_value_in
Sourceval pf_conv_x : Evar.t Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
  • deprecated Use the version in Tacmach.New
Sourceval pr_gls : Evar.t Evd.sigma -> Pp.t

Pretty-printing functions (debug only).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct