package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception FailError of int * Pp.t Stdlib.Lazy.t

A special exception for levels for the Fail tactic

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 tclSHOWHYPS : 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
Elimination tacticals.
val get_and_check_or_and_pattern : ?loc:Loc.t -> Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr -> bool list array -> Tactypes.intro_patterns array

get_and_check_or_and_pattern loc pats branchsign returns an appropriate error message if |pats| <> |branchsign|; extends them if no pattern is given for let-ins in the case of a conjunctive pattern

Tolerate "" to mean a disjunctive pattern of any length

val compute_constructor_signatures : rec_flag:bool -> (Names.inductive * 'a) -> bool list array
val compute_induction_names : bool -> bool list array -> Tactypes.or_and_intro_pattern option -> Tactypes.intro_patterns array

Useful for as intro_pattern modifier

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

Tacticals defined directly in term of Proofview

module New : sig ... end

The tacticals in the module New are the tactical of Ltac. Their semantics is an extension of the tacticals in this file for the multi-goal backtracking tactics. They do not have the same semantics as the similarly named tacticals in Proofview. The tactical of Proofview are used in the definition of the tacticals of Tacticals.New, but they are more atomic. In particular Tacticals.New.tclORELSE sees lack of progress as a failure, whereas Proofview.tclORELSE doesn't. Additionally every tactic which can catch failure (tclOR, tclORELSE, tclTRY, tclREPEAt, etc…) are run into each goal independently (failures and backtracks are localised to a given goal).

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