package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val locate_tactic : Libnames.qualid -> Tacexpr.ltac_constant
val locate_extended_all_tactic : Libnames.qualid -> Tacexpr.ltac_constant list
val exists_tactic : Libnames.full_path -> bool
val shortest_qualid_of_tactic : Tacexpr.ltac_constant -> Libnames.qualid
type alias = Names.KerName.t
type alias_tactic = {
  1. alias_args : Names.Id.t list;
  2. alias_body : Tacexpr.glob_tactic_expr;
  3. alias_deprecation : Vernacinterp.deprecation option;
}
val register_alias : alias -> alias_tactic -> unit
val interp_alias : alias -> alias_tactic
val check_alias : alias -> bool
val register_ltac : bool -> bool -> ?deprecation:Vernacinterp.deprecation -> Names.Id.t -> Tacexpr.glob_tactic_expr -> unit
val redefine_ltac : bool -> ?deprecation:Vernacinterp.deprecation -> Names.KerName.t -> Tacexpr.glob_tactic_expr -> unit
val is_ltac_for_ml_tactic : Names.KerName.t -> bool
val tac_deprecation : Names.KerName.t -> Vernacinterp.deprecation option
type ltac_entry = {
  1. tac_for_ml : bool;
  2. tac_body : Tacexpr.glob_tactic_expr;
  3. tac_redef : Names.ModPath.t list;
  4. tac_deprecation : Vernacinterp.deprecation option;
}
val ltac_entries : unit -> ltac_entry Names.KNmap.t
type ml_tactic = Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic
val register_ml_tactic : ?overwrite:bool -> Tacexpr.ml_tactic_name -> ml_tactic array -> unit
val interp_ml_tactic : Tacexpr.ml_tactic_entry -> ml_tactic
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