Module Tacticals.Old

val catch_failerror : Exninfo.iexn -> unit

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

type tactic = Proofview.V82.tac
val tclIDTAC : tactic
val tclIDTAC_MESSAGE : Pp.t -> tactic
val tclORELSE0 : tactic -> tactic -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHENLIST : tactic list -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENFIRST : tactic -> tactic -> tactic
val tclTHENLAST : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclTHENSV : tactic -> tactic array -> tactic
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
val tclREPEAT : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> Pp.t -> tactic
val tclFAIL_lazy : int -> Pp.t Stdlib.Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
Tacticals applying to hypotheses
val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic
val onNthHyp : int -> (EConstr.constr -> tactic) -> tactic
val onNthDecl : int -> (EConstr.named_declaration -> tactic) -> tactic
val onLastHypId : (Names.Id.t -> tactic) -> tactic
val onLastHyp : (EConstr.constr -> tactic) -> tactic
val onLastDecl : (EConstr.named_declaration -> tactic) -> tactic
val onNLastHypsId : int -> (Names.Id.t list -> tactic) -> tactic
val onNLastHyps : int -> (EConstr.constr list -> tactic) -> tactic
val onNLastDecls : int -> (EConstr.named_context -> tactic) -> tactic
val lastHypId : Goal.goal Evd.sigma -> Names.Id.t
val lastHyp : Goal.goal Evd.sigma -> EConstr.constr
val lastDecl : Goal.goal Evd.sigma -> EConstr.named_declaration
val nLastHypsId : int -> Goal.goal Evd.sigma -> Names.Id.t list
val nLastHyps : int -> Goal.goal Evd.sigma -> EConstr.constr list
val nLastDecls : int -> Goal.goal Evd.sigma -> EConstr.named_context
val afterHyp : Names.Id.t -> Goal.goal Evd.sigma -> EConstr.named_context
val ifOnHyp : ((Names.Id.t * EConstr.types) -> bool) -> (Names.Id.t -> tactic) -> (Names.Id.t -> tactic) -> Names.Id.t -> tactic
val onHyps : (Goal.goal Evd.sigma -> EConstr.named_context) -> (EConstr.named_context -> tactic) -> tactic
Tacticals applying to goal components
val onAllHyps : (Names.Id.t -> tactic) -> tactic
val onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic
val onClause : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
val onClauseLR : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
val elimination_sort_of_goal : Goal.goal Evd.sigma -> Sorts.family
val elimination_sort_of_hyp : Names.Id.t -> Goal.goal Evd.sigma -> Sorts.family
val elimination_sort_of_clause : Names.Id.t option -> Goal.goal Evd.sigma -> Sorts.family
val pf_with_evars : (Goal.goal Evd.sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
val pf_constr_of_global : Names.GlobRef.t -> (EConstr.constr -> tactic) -> tactic