package coq-serapi

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Id : sig ... end
module Name : sig ... end
module DirPath : sig ... end
module Label : sig ... end
module MBId : sig ... end
module ModPath : sig ... end
module KerName : sig ... end
module Constant : sig ... end
module MutInd : sig ... end
type 'a tableKey = 'a Names.tableKey
val tableKey_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a tableKey
val sexp_of_tableKey : ('a -> Sexplib.Sexp.t) -> 'a tableKey -> Sexplib.Sexp.t
type variable = Names.variable
type inductive = Names.inductive
type constructor = Names.constructor
module Projection : sig ... end
type projection = Names.Projection.t
module GlobRef : sig ... end
val variable_of_sexp : Sexplib.Sexp.t -> variable
val sexp_of_variable : variable -> Sexplib.Sexp.t
val inductive_of_sexp : Sexplib.Sexp.t -> inductive
val sexp_of_inductive : inductive -> Sexplib.Sexp.t
val constructor_of_sexp : Sexplib.Sexp.t -> constructor
val sexp_of_constructor : constructor -> Sexplib.Sexp.t
val projection_of_sexp : Sexplib.Sexp.t -> projection
val sexp_of_projection : projection -> Sexplib.Sexp.t
type evaluable_global_reference = Names.evaluable_global_reference
val evaluable_global_reference_of_sexp : Sexplib.Sexp.t -> evaluable_global_reference
val sexp_of_evaluable_global_reference : evaluable_global_reference -> Sexplib.Sexp.t
type lident = Names.lident
val lident_of_sexp : Sexplib.Sexp.t -> lident
val sexp_of_lident : lident -> Sexplib.Sexp.t
type lname = Names.lname
val lname_of_sexp : Sexplib.Sexp.t -> lname
val sexp_of_lname : lname -> Sexplib.Sexp.t
type lstring = Names.lstring
val lstring_of_sexp : Sexplib.Sexp.t -> lstring
val sexp_of_lstring : lstring -> Sexplib.Sexp.t
OCaml

Innovation. Community. Security.