package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
val test_lpar_idnum_coloneq : unit Pcoq.Entry.t
val test_lpar_id_colon : unit Pcoq.Entry.t
val test_lpar_id_coloneq : unit Pcoq.Entry.t
val test_lpar_id_rpar : unit Pcoq.Entry.t
val test_ampersand_ident : unit Pcoq.Entry.t
val test_dollar_ident : unit Pcoq.Entry.t
val test_ltac1_env : unit Pcoq.Entry.t
val test_ident_with_or_lpar_or_rbrac : unit Pcoq.Entry.t
val test_array_opening : unit Pcoq.Entry.t
val test_array_closing : unit Pcoq.Entry.t
val test_leftsquarebracket_equal : unit Pcoq.Entry.t
val _ltac2_expr : Tac2expr.raw_tacexpr Pcoq.Entry.t
val tac2def_val : Tac2expr.strexpr Pcoq.Entry.t
val tac2def_typ : Tac2expr.strexpr Pcoq.Entry.t
val tac2def_ext : Tac2expr.strexpr Pcoq.Entry.t
val tac2def_syn : (Tac2expr.sexpr list * int option * Tac2expr.raw_tacexpr) Pcoq.Entry.t
val tac2def_mut : Tac2expr.strexpr Pcoq.Entry.t
val tac2expr_in_env : (Names.Id.t CAst.t list * Tac2expr.raw_tacexpr) Pcoq.Entry.t
val wit_ltac2_entry : (Tac2expr.strexpr, unit, unit) Genarg.genarg_type
val ltac2_entry : Tac2expr.strexpr Pcoq.Entry.t
val wit_ltac2def_syn : (Tac2expr.sexpr list * int option * Tac2expr.raw_tacexpr, unit, unit) Genarg.genarg_type
val ltac2def_syn : (Tac2expr.sexpr list * int option * Tac2expr.raw_tacexpr) Pcoq.Entry.t
val wit_ltac2_expr : (Tac2expr.raw_tacexpr, unit, unit) Genarg.genarg_type
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