package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a sigma = 'a Evd.sigma
type tactic = Proof_type.tactic
val sig_it : 'a sigma -> 'a
val re_sig : 'a -> Evd.evar_map -> 'a sigma
val unpackage : 'a sigma -> Evd.evar_map ref * 'a
val repackage : Evd.evar_map ref -> 'a -> 'a sigma
val pf_hyps_types : Proof_type.goal sigma -> (Names.Id.t * EConstr.types) list
val pf_nth_hyp_id : Proof_type.goal sigma -> int -> Names.Id.t
val pf_ids_of_hyps : Proof_type.goal sigma -> Names.Id.t list
val pf_unsafe_type_of : Proof_type.goal sigma -> EConstr.constr -> EConstr.types
val pf_get_hyp_typ : Proof_type.goal sigma -> Names.Id.t -> EConstr.types
val pf_get_new_id : Names.Id.t -> Proof_type.goal sigma -> Names.Id.t
val pf_get_new_ids : Names.Id.t list -> Proof_type.goal sigma -> Names.Id.t list
val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Proof_type.goal sigma -> 'a
val pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> Proof_type.goal sigma -> 'a -> Proof_type.goal sigma * 'b
val pf_conv_x : Proof_type.goal sigma -> EConstr.constr -> EConstr.constr -> bool
val pf_conv_x_leq : Proof_type.goal sigma -> EConstr.constr -> EConstr.constr -> bool
val pf_is_matching : Proof_type.goal sigma -> Pattern.constr_pattern -> EConstr.constr -> bool
val refiner : Proof_type.rule -> tactic
val internal_cut_no_check : bool -> Names.Id.t -> EConstr.types -> tactic
val refine_no_check : EConstr.constr -> tactic
val internal_cut : bool -> Names.Id.t -> EConstr.types -> tactic
val internal_cut_rev : bool -> Names.Id.t -> EConstr.types -> tactic
val refine : EConstr.constr -> tactic
val pr_glls : Proof_type.goal list sigma -> Pp.std_ppcmds
module New : sig ... end
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