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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct