package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
val genarg_of_unit : unit -> Genarg.rlevel Genarg.generic_argument
val genarg_of_int : int -> Genarg.rlevel Genarg.generic_argument
val toplevel_selector : Goal_select.t Pcoq.Entry.t
val tacdef_body : Tacexpr.tacdef_body Pcoq.Entry.t
val classic_proof_mode : Pvernac.proof_mode
val test_bracket_ident : unit Pcoq.Entry.t
val wit_ltac_selector : (Goal_select.t, unit, unit) Genarg.genarg_type
val ltac_selector : Goal_select.t Pcoq.Entry.t
val wit_ltac_info : (int, unit, unit) Genarg.genarg_type
val ltac_info : int Pcoq.Entry.t
val wit_ltac_use_default : (bool, unit, unit) Genarg.genarg_type
val ltac_use_default : bool Pcoq.Entry.t
val wit_ltac_tactic_level : (int, unit, unit) Genarg.genarg_type
val ltac_tactic_level : int Pcoq.Entry.t
val wit_ltac_production_sep : (string, unit, unit) Genarg.genarg_type
val ltac_production_sep : string Pcoq.Entry.t
val wit_ltac_production_item : ((string * string option) Tacentries.grammar_tactic_prod_item_expr, unit, unit) Genarg.genarg_type
val ltac_production_item : (string * string option) Tacentries.grammar_tactic_prod_item_expr Pcoq.Entry.t
val wit_ltac_tacdef_body : (Tacexpr.tacdef_body, unit, unit) Genarg.genarg_type
val ltac_tacdef_body : Tacexpr.tacdef_body Pcoq.Entry.t
val for_extraargs : unit

extraargs needs g_ltac to initialize tactic_value

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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