package coq

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

Module Tacticals.NewSource

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).

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 tclFAIL : ?info:Exninfo.info -> int -> Pp.t -> 'a Proofview.tactic
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 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 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]
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