package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val catch_failerror : Exninfo.iexn -> unit

Takes an exception and either raise it at the next level or do nothing.

Tacticals i.e. functions from tactics to tactics.

type tactic = Proofview.V82.tac
val tclIDTAC : tactic
val tclIDTAC_MESSAGE : Pp.t -> tactic
val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHENLIST : tactic list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENFIRST : tactic -> tactic -> tactic
val tclTHENLAST : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclTHENSV : tactic -> tactic array -> tactic
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
val tclREPEAT : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.t -> tactic
val tclFAIL_lazy : int -> Pp.t Stdlib.Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
Tacticals applying to hypotheses
val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic
val onNthHyp : int -> (EConstr.constr -> tactic) -> tactic
val onNthDecl : int -> (EConstr.named_declaration -> tactic) -> tactic
val onLastHypId : (Names.Id.t -> tactic) -> tactic
val onLastHyp : (EConstr.constr -> tactic) -> tactic
val onLastDecl : (EConstr.named_declaration -> tactic) -> tactic
val onNLastHypsId : int -> (Names.Id.t list -> tactic) -> tactic
val onNLastHyps : int -> (EConstr.constr list -> tactic) -> tactic
val onNLastDecls : int -> (EConstr.named_context -> tactic) -> tactic
val lastHypId : Goal.goal Evd.sigma -> Names.Id.t
val nLastHypsId : int -> Goal.goal Evd.sigma -> Names.Id.t list
val nLastHyps : int -> Goal.goal Evd.sigma -> EConstr.constr list
val nLastDecls : int -> Goal.goal Evd.sigma -> EConstr.named_context
val ifOnHyp : ((Names.Id.t * EConstr.types) -> bool) -> (Names.Id.t -> tactic) -> (Names.Id.t -> tactic) -> Names.Id.t -> tactic
Tacticals applying to goal components

A clause denotes occurrences and hypotheses in a goal; in particular, it can abstractly refer to the set of hypotheses independently of the effective contents of the current goal

val onAllHyps : (Names.Id.t -> tactic) -> tactic
val onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic
val onClause : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
val onClauseLR : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
val elimination_sort_of_goal : Goal.goal Evd.sigma -> Sorts.family
val elimination_sort_of_hyp : Names.Id.t -> Goal.goal Evd.sigma -> Sorts.family
val elimination_sort_of_clause : Names.Id.t option -> Goal.goal Evd.sigma -> Sorts.family
val pf_with_evars : (Goal.goal Evd.sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
val pf_constr_of_global : Names.GlobRef.t -> (EConstr.constr -> tactic) -> 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