package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception FailError of int * Pp.t Lazy.t
val catch_failerror : Exninfo.iexn -> unit
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 Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclSHOWHYPS : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
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 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 ifOnHyp : ((Names.Id.t * EConstr.types) -> bool) -> (Names.Id.t -> tactic) -> (Names.Id.t -> tactic) -> Names.Id.t -> tactic
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 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 array
val compute_constructor_signatures : rec_flag:bool -> (Names.inductive * 'a) -> bool list array
val compute_induction_names : bool -> bool list array -> Tactypes.or_and_intro_pattern option -> Tactypes.intro_patterns array
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
module New : sig ... end