package coq

  1. Overview
  2. Docs
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.