package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module TacticalsSource

Sourceexception FailError of int * Pp.t Lazy.t

A special exception for levels for the Fail tactic

Tacticals defined directly in term of Proofview

The tacticals below 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, but they are more atomic. In particular Tacticals.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).

Sourceval catch_failerror : Exninfo.iexn -> unit Proofview.tactic

catch_failerror e fails and decreases the level if e is an Ltac error with level more than 0. Otherwise succeeds.

Sourceval tclIDTAC : unit Proofview.tactic
Sourceval tclTHEN : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclFAILn : ?info:Exninfo.info -> int -> Pp.t -> 'a Proofview.tactic
Sourceval tclFAIL : ?info:Exninfo.info -> Pp.t -> 'a Proofview.tactic

Same as above with level set to 0.

Sourceval tclZEROMSG : ?info:Exninfo.info -> ?loc:Loc.t -> Pp.t -> 'a Proofview.tactic

Fail with a User_Error containing the given message.

Sourceval tclORD : unit Proofview.tactic -> (unit -> unit Proofview.tactic) -> unit Proofview.tactic

Like tclOR but accepts a delayed tactic as a second argument in the form of a function which will be run only in case of backtracking.

Sourceval tclONCE : unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclEXACTLY_ONCE : unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclIFCATCH : unit Proofview.tactic -> (unit -> unit Proofview.tactic) -> (unit -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval tclORELSE0 : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclORELSE : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclTHENS3PARTS : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic

tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls applies the tactic tac1 to gls then, applies t1, ..., tn to the first n resulting subgoals, t'1, ..., t'm to the last m subgoals and tac2 to the rest of the subgoals in the middle. Raises an error if the number of resulting subgoals is strictly less than n+m

Sourceval tclTHENSLASTn : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic
Sourceval tclTHENSFIRSTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclTHENFIRSTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic
Sourceval tclTHENFIRST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic

tclTHENFIRST tac1 tac2 gls applies the tactic tac1 to gls and tac2 to the first resulting subgoal

Sourceval tclBINDFIRST : 'a Proofview.tactic -> ('a -> 'b Proofview.tactic) -> 'b Proofview.tactic
Sourceval tclTHENLASTn : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic
Sourceval tclTHENLAST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclBINDLAST : 'a Proofview.tactic -> ('a -> 'b Proofview.tactic) -> 'b Proofview.tactic
Sourceval tclTHENS : unit Proofview.tactic -> unit Proofview.tactic list -> unit Proofview.tactic
Sourceval tclTHENLIST : unit Proofview.tactic list -> unit Proofview.tactic
Sourceval tclMAP : ('a -> unit Proofview.tactic) -> 'a list -> unit Proofview.tactic

tclMAP f [x1..xn] builds (f x1);(f x2);...(f xn)

Sourceval tclTRY : unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclTRYb : unit Proofview.tactic -> bool list Proofview.tactic
Sourceval tclFIRST : unit Proofview.tactic list -> unit Proofview.tactic
Sourceval tclIFTHENELSE : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclIFTHENSVELSE : unit Proofview.tactic -> unit Proofview.tactic array -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclIFTHENTRYELSEMUST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclIFTHENFIRSTTRYELSEMUST : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclDO : int -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclREPEAT : unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclREPEAT_MAIN : unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclCOMPLETE : 'a Proofview.tactic -> 'a Proofview.tactic
Sourceval tclSOLVE : unit Proofview.tactic list -> unit Proofview.tactic
Sourceval tclPROGRESS : unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclRUNWITHHOLES : bool -> 'a Proofview.tactic -> ('a -> 'b Proofview.tactic) -> 'b Proofview.tactic

tclRUNWITHHOLES b tac0 tac is tac0 >>= tac if b = false, otherwise it additionally checks that evars created by tac0 are solved after tac.

Sourceval tclWITHHOLES : bool -> 'a Proofview.tactic -> Evd.evar_map -> 'a Proofview.tactic
Sourceval tclDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval tclMAPDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open list -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval tactic_of_delayed : 'a Tactypes.delayed_open -> 'a Proofview.tactic

Must be focused to use

Sourceval check_evar_list : Environ.env -> Evd.evar_map -> Evar.Set.t -> Evd.evar_map -> Evar.t list
Sourceval tclTIMEOUT : int -> unit Proofview.tactic -> unit Proofview.tactic
Sourceval tclTIME : string option -> 'a Proofview.tactic -> 'a Proofview.tactic
Sourceval onNthHypId : int -> (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval onLastHypId : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval onLastHyp : (EConstr.constr -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval onNLastHypsId : int -> (Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval onNLastHyps : int -> (EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval onNLastDecls : int -> (EConstr.named_context -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval tryAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval tryAllHypsAndConcl : (Names.Id.t option -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval onClause : (Names.Id.t option -> unit Proofview.tactic) -> Locus.clause -> unit Proofview.tactic
Sourceval onAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval onAllHypsAndConcl : (Names.Id.t option -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family
Sourceval elimination_sort_of_hyp : Names.Id.t -> Proofview.Goal.t -> Sorts.family
Sourceval elimination_sort_of_clause : Names.Id.t option -> Proofview.Goal.t -> Sorts.family
Sourceval tclTYPEOFTHEN : ?refresh:bool -> EConstr.constr -> (Evd.evar_map -> EConstr.types -> unit Proofview.tactic) -> unit Proofview.tactic
Sourceval tclSELECT : ?nosuchgoal:'a Proofview.tactic -> Goal_select.t -> 'a Proofview.tactic -> 'a Proofview.tactic
  • deprecated Use [Goal_select.tclSELECT]
Elimination tacticals.
Sourceval 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

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

Useful for as intro_pattern modifier

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