Old (p.coq.8.15.2.doc.coq-core.tactics.Tacticals.Old)

Sourceval catch_failerror : Exninfo.iexn -> unit

Takes an exception and either raise it at the next level or do nothing.

Tacticals i.e. functions from tactics to tactics.

Sourcetype tactic = Evar.t Evd.sigma -> Evar.t list Evd.sigma

Sourceval tclIDTAC : tactic

Sourceval tclIDTAC_MESSAGE : Pp.t -> tactic

Sourceval tclORELSE0 : tactic -> tactic -> tactic

Sourceval tclORELSE : tactic -> tactic -> tactic

Sourceval tclTHEN : tactic -> tactic -> tactic

Sourceval tclTHENLIST : tactic list -> tactic

Sourceval tclTHEN_i : tactic -> (int -> tactic) -> tactic

Sourceval tclTHENFIRST : tactic -> tactic -> tactic

Sourceval tclTHENLAST : tactic -> tactic -> tactic

Sourceval tclTHENS : tactic -> tactic list -> tactic

Sourceval tclTHENSV : tactic -> tactic array -> tactic

Sourceval tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic

Sourceval tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic

Sourceval tclREPEAT : tactic -> tactic

Sourceval tclFIRST : tactic list -> tactic

Sourceval tclTRY : tactic -> tactic

Sourceval tclCOMPLETE : tactic -> tactic

Sourceval tclAT_LEAST_ONCE : tactic -> tactic

Sourceval tclFAIL : int -> Pp.t -> tactic

Sourceval tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic

Sourceval tclDO : int -> tactic -> tactic

Sourceval tclPROGRESS : tactic -> tactic

Sourceval tclTHENTRY : tactic -> tactic -> tactic

Sourceval tclMAP : ('a -> tactic) -> 'a list -> tactic

Tacticals applying to hypotheses

Sourceval onNthHypId : int -> (Names.Id.t -> tactic) -> tactic

Sourceval onNthHyp : int -> (EConstr.constr -> tactic) -> tactic

Sourceval onNthDecl : int -> (EConstr.named_declaration -> tactic) -> tactic

Sourceval onLastHypId : (Names.Id.t -> tactic) -> tactic

Sourceval onLastHyp : (EConstr.constr -> tactic) -> tactic

Sourceval onLastDecl : (EConstr.named_declaration -> tactic) -> tactic

Sourceval onNLastHypsId : int -> (Names.Id.t list -> tactic) -> tactic

Sourceval onNLastHyps : int -> (EConstr.constr list -> tactic) -> tactic

Sourceval onNLastDecls : int -> (EConstr.named_context -> tactic) -> tactic

Sourceval lastHypId : Goal.goal Evd.sigma -> Names.Id.t

Sourceval lastHyp : Goal.goal Evd.sigma -> EConstr.constr

Sourceval lastDecl : Goal.goal Evd.sigma -> EConstr.named_declaration

Sourceval nLastHypsId : int -> Goal.goal Evd.sigma -> Names.Id.t list

Sourceval nLastHyps : int -> Goal.goal Evd.sigma -> EConstr.constr list

Sourceval nLastDecls : int -> Goal.goal Evd.sigma -> EConstr.named_context

Sourceval afterHyp : Names.Id.t -> Goal.goal Evd.sigma -> EConstr.named_context

Source

val ifOnHyp : 
  ((Names.Id.t * EConstr.types) -> bool) ->
  (Names.Id.t -> tactic) ->
  (Names.Id.t -> tactic) ->
  Names.Id.t ->
  tactic

Source

val onHyps : 
  (Goal.goal Evd.sigma -> EConstr.named_context) ->
  (EConstr.named_context -> tactic) ->
  tactic

Tacticals 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

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

Sourceval onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic

Sourceval onClause : (Names.Id.t option -> tactic) -> Locus.clause -> tactic

Sourceval onClauseLR : (Names.Id.t option -> tactic) -> Locus.clause -> tactic

Sourceval elimination_sort_of_goal : Goal.goal Evd.sigma -> Sorts.family

Sourceval elimination_sort_of_hyp : Names.Id.t -> Goal.goal Evd.sigma -> Sorts.family

Source

val elimination_sort_of_clause : 
  Names.Id.t option ->
  Goal.goal Evd.sigma ->
  Sorts.family

Source

val pf_with_evars : 
  (Goal.goal Evd.sigma -> Evd.evar_map * 'a) ->
  ('a -> tactic) ->
  tactic

Source

val pf_constr_of_global : 
  Names.GlobRef.t ->
  (EConstr.constr -> tactic) ->
  tactic