package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val catch_failerror : Util.iexn -> unit Proofview.tactic
val tclIDTAC : unit Proofview.tactic
val tclTHEN : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclFAIL : int -> Pp.t -> 'a Proofview.tactic
val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a Proofview.tactic
val tclOR : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclORD : unit Proofview.tactic -> (unit -> unit Proofview.tactic) -> unit Proofview.tactic
val tclONCE : unit Proofview.tactic -> unit Proofview.tactic
val tclEXACTLY_ONCE : unit Proofview.tactic -> unit Proofview.tactic
val tclIFCATCH : unit Proofview.tactic -> (unit -> unit Proofview.tactic) -> (unit -> unit Proofview.tactic) -> unit Proofview.tactic
val tclORELSE0 : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclORELSE : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclTHENS3PARTS : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic
val tclTHENSFIRSTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tactic
val tclTHENFIRSTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic
val tclTHENFIRST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclBINDFIRST : 'a Proofview.tactic -> ('a -> 'b Proofview.tactic) -> 'b Proofview.tactic
val tclTHENLASTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic
val tclTHENLAST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclBINDLAST : 'a Proofview.tactic -> ('a -> 'b Proofview.tactic) -> 'b Proofview.tactic
val tclTHENS : unit Proofview.tactic -> unit Proofview.tactic list -> unit Proofview.tactic
val tclTHENLIST : unit Proofview.tactic list -> unit Proofview.tactic
val tclMAP : ('a -> unit Proofview.tactic) -> 'a list -> unit Proofview.tactic
val tclTRY : unit Proofview.tactic -> unit Proofview.tactic
val tclTRYb : unit Proofview.tactic -> bool list Proofview.tactic
val tclFIRST : unit Proofview.tactic list -> unit Proofview.tactic
val tclIFTHENELSE : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclIFTHENSVELSE : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tactic
val tclIFTHENTRYELSEMUST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclIFTHENFIRSTTRYELSEMUST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclDO : int -> unit Proofview.tactic -> unit Proofview.tactic
val tclREPEAT : unit Proofview.tactic -> unit Proofview.tactic
val tclREPEAT_MAIN : unit Proofview.tactic -> unit Proofview.tactic
val tclCOMPLETE : 'a Proofview.tactic -> 'a Proofview.tactic
val tclSOLVE : unit Proofview.tactic list -> unit Proofview.tactic
val tclPROGRESS : unit Proofview.tactic -> unit Proofview.tactic
val tclSELECT : Goal_select.t -> 'a Proofview.tactic -> 'a Proofview.tactic
val tclWITHHOLES : bool -> 'a Proofview.tactic -> Evd.evar_map -> 'a Proofview.tactic
val tclDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
val tclTIMEOUT : int -> unit Proofview.tactic -> unit Proofview.tactic
val tclTIME : string option -> 'a Proofview.tactic -> 'a Proofview.tactic
val nLastDecls : Proofview.Goal.t -> int -> EConstr.named_context
val ifOnHyp : ((Names.Id.t * EConstr.types) -> bool) -> (Names.Id.t -> unit Proofview.tactic) -> (Names.Id.t -> unit Proofview.tactic) -> Names.Id.t -> unit Proofview.tactic
val onNthHypId : int -> (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val onLastHypId : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val onLastHyp : (EConstr.constr -> unit Proofview.tactic) -> unit Proofview.tactic
val tryAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val tryAllHypsAndConcl : (Names.Id.t option -> unit Proofview.tactic) -> unit Proofview.tactic
val onClause : (Names.Id.t option -> unit Proofview.tactic) -> Locus.clause -> unit Proofview.tactic
val elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family
val elimination_sort_of_hyp : Names.Id.t -> Proofview.Goal.t -> Sorts.family
val elimination_sort_of_clause : Names.Id.t option -> Proofview.Goal.t -> Sorts.family
val elimination_then : (branch_args -> unit Proofview.tactic) -> EConstr.constr -> unit Proofview.tactic
val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic
val pf_constr_of_global : Names.GlobRef.t -> EConstr.constr Proofview.tactic