package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587

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

Module Tacticals.OldSource

  • deprecated Use the new engine
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 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 : Evar.t Evd.sigma -> Names.Id.t
Sourceval nLastHypsId : int -> Evar.t Evd.sigma -> Names.Id.t list
Sourceval nLastHyps : int -> Evar.t Evd.sigma -> EConstr.constr list
Sourceval nLastDecls : int -> Evar.t Evd.sigma -> EConstr.named_context
Sourceval ifOnHyp : ((Names.Id.t * EConstr.types) -> bool) -> (Names.Id.t -> tactic) -> (Names.Id.t -> tactic) -> Names.Id.t -> 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 : Evar.t Evd.sigma -> Sorts.family
Sourceval elimination_sort_of_hyp : Names.Id.t -> Evar.t Evd.sigma -> Sorts.family
Sourceval elimination_sort_of_clause : Names.Id.t option -> Evar.t Evd.sigma -> Sorts.family
Sourceval pf_with_evars : (Goal.goal Evd.sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
Sourceval pf_constr_of_global : Names.GlobRef.t -> (EConstr.constr -> tactic) -> tactic