package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a sigma = 'a Evd.sigma
  • deprecated alias of Evd.sigma
type tactic = Proof_type.tactic
val sig_it : 'a Evd.sigma -> 'a
val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma
val unpackage : 'a Evd.sigma -> Evd.evar_map ref * 'a
  • deprecated Do not use [evar_map ref]
val repackage : Evd.evar_map ref -> 'a -> 'a Evd.sigma
  • deprecated Do not use [evar_map ref]
  • deprecated Do not use [evar_map ref]
val pf_hyps_types : Proof_type.goal Evd.sigma -> (Names.Id.t * EConstr.types) list
val pf_nth_hyp_id : Proof_type.goal Evd.sigma -> int -> Names.Id.t
val pf_ids_of_hyps : Proof_type.goal Evd.sigma -> Names.Id.t list
val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Proof_type.goal Evd.sigma -> 'a
val pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> Proof_type.goal Evd.sigma -> 'a -> Proof_type.goal Evd.sigma * 'b
val pf_conv_x_leq : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool
val refiner : Proof_type.rule -> tactic
val refine_no_check : EConstr.constr -> tactic
val refine : EConstr.constr -> tactic
val pr_glls : Proof_type.goal list Evd.sigma -> Pp.t
module New : sig ... end