package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

dune-project

Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

T

The Coq development team, INRIA, CNRS, and contributors.

Maintainers

C

coqdev@inria.fr

Sources

coq-8.14.1.tar.gz

sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/coq-core.tactics/Tacticals/New/index.html

Module `Tacticals.New`Source

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

val tclTHEN : 
  unit Proofview.tactic ->
  unit Proofview.tactic ->
  unit Proofview.tactic

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

Sourceval tclONCE : unit Proofview.tactic -> unit Proofview.tactic

Sourceval 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

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

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

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

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

Sourceval tclTIMEOUT : int -> unit Proofview.tactic -> unit Proofview.tactic

Sourceval tclTIME : string option -> 'a Proofview.tactic -> 'a Proofview.tactic

Sourceval nLastDecls : Proofview.Goal.t -> int -> EConstr.named_context

val ifOnHyp : 
  (Environ.env -> Evd.evar_map -> (Names.Id.t * EConstr.types) -> bool) ->
  (Names.Id.t -> unit Proofview.tactic) ->
  (Names.Id.t -> unit Proofview.tactic) ->
  Names.Id.t ->
  unit Proofview.tactic

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 onLastDecl : 
  (EConstr.named_declaration -> 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 onHyps : 
  (Proofview.Goal.t -> EConstr.named_context) ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

val afterHyp : 
  Names.Id.t ->
  (EConstr.named_context -> unit Proofview.tactic) ->
  unit Proofview.tactic

Sourceval 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

Sourceval onAllHyps : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic

val 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

val elimination_sort_of_clause : 
  Names.Id.t option ->
  Proofview.Goal.t ->
  Sorts.family

Sourceval 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]