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

module Old : sig ... end

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

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

val tclIDTAC : unit Proofview.tactic
val tclTHEN : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val tclFAIL : ?info:Exninfo.info -> int -> Pp.t -> 'a Proofview.tactic
val tclZEROMSG : ?info:Exninfo.info -> ?loc:Loc.t -> Pp.t -> 'a Proofview.tactic

Fail with a User_Error containing the given message.

val tclOR : unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic
val 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.

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

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

val tclTHENSLASTn : unit Proofview.tactic -> 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

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

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

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

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 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 tclMAPDELAYEDWITHHOLES : bool -> 'a Tactypes.delayed_open list -> ('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 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 onNLastHypsId : int -> (Names.Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic
val onNLastHyps : int -> (EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic
val onNLastDecls : int -> (EConstr.named_context -> 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 onAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val onAllHypsAndConcl : (Names.Id.t option -> unit Proofview.tactic) -> 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 pf_constr_of_global : Names.GlobRef.t -> EConstr.constr Proofview.tactic
val tclTYPEOFTHEN : ?refresh:bool -> EConstr.constr -> (Evd.evar_map -> EConstr.types -> unit Proofview.tactic) -> unit Proofview.tactic
val tclSELECT : ?nosuchgoal:'a Proofview.tactic -> Goal_select.t -> 'a Proofview.tactic -> 'a Proofview.tactic
  • deprecated Use [Goal_select.tclSELECT]
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 : Environ.env -> 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

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