package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val ldots_var : Names.Id.t
val constr_kw : string list
val binders_of_names : (Loc.t option * Names.Name.t) list -> Constrexpr.local_binder_expr list
val mk_fixb : ('a * 'b * 'c * 'd * ('e * Constrexpr.constr_expr_r CAst.t option)) -> 'a * 'c * 'b * Constrexpr.constr_expr_r CAst.t * 'd
val mk_cofixb : ('a * 'b * ((Loc.t option * 'c) option * 'd) * 'e * ('f * Constrexpr.constr_expr_r CAst.t option)) -> 'a * 'b * Constrexpr.constr_expr_r CAst.t * 'e
val err : unit -> 'a
val lpar_id_coloneq : Names.Id.t Pcoq.Gram.Entry.e
val impl_ident_head : Names.Id.t Pcoq.Gram.Entry.e
val name_colon : Names.name Pcoq.Gram.Entry.e
val aliasvar : Constrexpr.cases_pattern_expr_r CAst.t -> (Loc.t option * Names.name) option
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