package coq
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/coq-core.tactics/Tacticals/index.html
Module TacticalsSource
Takes an exception and either raise it at the next level or do nothing.
Tacticals i.e. functions from tactics to tactics.
Tacticals applying to hypotheses
val ifOnHyp :
((Names.Id.t * EConstr.types) -> bool) ->
(Names.Id.t -> tactic) ->
(Names.Id.t -> tactic) ->
Names.Id.t ->
tacticval onHyps :
(Goal.goal Evd.sigma -> EConstr.named_context) ->
(EConstr.named_context -> tactic) ->
tacticTacticals 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
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 arrayget_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
val fix_empty_or_and_pattern :
int ->
Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_expr ->
Tactypes.delayed_open_constr Tactypes.or_and_intro_pattern_exprTolerate "" to mean a disjunctive pattern of any length
val compute_constructor_signatures :
rec_flag:bool ->
(Names.inductive * 'a) ->
bool list arrayval compute_induction_names :
bool ->
bool list array ->
Tactypes.or_and_intro_pattern option ->
Tactypes.intro_patterns arrayUseful for as intro_pattern modifier
Tacticals defined directly in term of Proofview
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).