package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type tactic = Proofview.V82.tac
val sig_it : 'a Evd.sigma -> 'a
val project : 'a Evd.sigma -> Evd.evar_map
val refiner : check:bool -> Constr.t -> tactic
val tclIDTAC : tactic
val tclIDTAC_MESSAGE : Pp.t -> tactic
val tclEVARS : Evd.evar_map -> tactic
val tclEVARUNIVCONTEXT : UState.t -> tactic
val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic
val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic
val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHENLIST : tactic list -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENLAST : tactic -> tactic -> tactic
val tclTHENFIRST : tactic -> tactic -> tactic
val tclTHENSV : tactic -> tactic array -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
val tclTHENLASTn : tactic -> tactic array -> tactic
val tclTHENFIRSTn : tactic -> tactic array -> tactic
exception FailError of int * Pp.t Lazy.t
val catch_failerror : Exninfo.iexn -> unit
val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclREPEAT : tactic -> tactic
val tclREPEAT_MAIN : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclSOLVE : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.t -> tactic
val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic
val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic
val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
OCaml

Innovation. Community. Security.