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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct