package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
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 : 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
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