package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val sig_it : 'a Evd.sigma -> 'a
val project : 'a Evd.sigma -> Evd.evar_map
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 tclIDTAC : Proof_type.tactic
val tclIDTAC_MESSAGE : Pp.t -> Proof_type.tactic
val tclEVARUNIVCONTEXT : UState.t -> Proof_type.tactic
val tclPUSHEVARUNIVCONTEXT : UState.t -> Proof_type.tactic
val tclPUSHCONSTRAINTS : Univ.Constraint.t -> Proof_type.tactic
val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic
val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic
val tclTHENFIRSTn : Proof_type.tactic -> Proof_type.tactic array -> Proof_type.tactic
exception FailError of int * Pp.t Lazy.t
val catch_failerror : Exninfo.iexn -> unit
val tclREPEAT_MAIN : Proof_type.tactic -> Proof_type.tactic
val tclFIRST : Proof_type.tactic list -> Proof_type.tactic
val tclSOLVE : Proof_type.tactic list -> Proof_type.tactic
val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic
val tclFAIL : int -> Pp.t -> Proof_type.tactic
val tclFAIL_lazy : int -> Pp.t Lazy.t -> Proof_type.tactic
val tclDO : int -> Proof_type.tactic -> Proof_type.tactic
val tclIFTHENTRYELSEMUST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic