package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val tclIDTAC : Proof_type.tactic
val tclIDTAC_MESSAGE : Pp.t -> Proof_type.tactic
val tclTHENSEQ : Proof_type.tactic list -> Proof_type.tactic
  • deprecated alias of Tacticals.tclTHENLIST
val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic
val tclTHENFIRSTn : Proof_type.tactic -> Proof_type.tactic array -> Proof_type.tactic
val tclREPEAT_MAIN : Proof_type.tactic -> Proof_type.tactic
val tclFIRST : Proof_type.tactic list -> Proof_type.tactic
val tclSOLVE : Proof_type.tactic list -> Proof_type.tactic
val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic
val tclFAIL : int -> Pp.t -> Proof_type.tactic
val tclFAIL_lazy : int -> Pp.t Lazy.t -> Proof_type.tactic
val tclDO : int -> Proof_type.tactic -> Proof_type.tactic
val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic
val tclIFTHENTRYELSEMUST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
val onNthHypId : int -> (Names.Id.t -> Proof_type.tactic) -> Proof_type.tactic
val onNthHyp : int -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic
val onNLastHypsId : int -> (Names.Id.t list -> Proof_type.tactic) -> Proof_type.tactic
val onNLastHyps : int -> (EConstr.constr list -> Proof_type.tactic) -> Proof_type.tactic
val nLastHypsId : int -> Proof_type.goal Evd.sigma -> Names.Id.t list
val nLastHyps : int -> Proof_type.goal Evd.sigma -> EConstr.constr list
val onAllHypsAndConcl : (Names.Id.t option -> Proof_type.tactic) -> Proof_type.tactic
val onClauseLR : (Names.Id.t option -> Proof_type.tactic) -> Locus.clause -> Proof_type.tactic
type branch_args = private {
  1. ity : Constr.pinductive;
  2. largs : EConstr.constr list;
  3. branchnum : int;
  4. pred : EConstr.constr;
  5. nassums : int;
  6. branchsign : bool list;
  7. branchnames : Tactypes.intro_patterns;
}
type branch_assumptions = private {
  1. ba : branch_args;
  2. assums : EConstr.named_context;
}
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 list array -> Tactypes.or_and_intro_pattern option -> Tactypes.intro_patterns array
val elimination_sort_of_goal : Proof_type.goal Evd.sigma -> Sorts.family
val elimination_sort_of_hyp : Names.Id.t -> Proof_type.goal Evd.sigma -> Sorts.family
val elimination_sort_of_clause : Names.Id.t option -> Proof_type.goal Evd.sigma -> Sorts.family
val pf_with_evars : (Proof_type.goal Evd.sigma -> Evd.evar_map * 'a) -> ('a -> Proof_type.tactic) -> Proof_type.tactic
module New : sig ... end