package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Id : sig ... end
module Name : SerType.SJHC with type t = Names.Name.t
module DirPath : SerType.SJHC with type t = Names.DirPath.t
module DPmap : Ser_cMap.ExtS with type key = DirPath.t and type 'a t = 'a Names.DPmap.t
module Label : SerType.SJHC with type t = Names.Label.t
module MBId : SerType.SJHC with type t = Names.MBId.t
module ModPath : SerType.SJHC with type t = Names.ModPath.t
module MPmap : Ser_cMap.ExtS with type key = ModPath.t and type 'a t = 'a Names.MPmap.t
module KerName : SerType.SJHC with type t = Names.KerName.t
module KNmap : Ser_cMap.ExtS with type key = KerName.t and type 'a t = 'a Names.KNmap.t
module Cset_env : Ser_cSet.ExtS with type elt = Constant.t and type t = Names.Cset_env.t
module Cmap : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap.t
module Cmap_env : Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap_env.t
module MutInd : SerType.SJHC with type t = Names.MutInd.t
module Mindmap : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap.t
module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap_env.t
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
val variable_to_yojson : variable -> Yojson.Safe.t
val sexp_of_variable : variable -> Sexplib0.Sexp.t
val variable_of_sexp : Sexplib0.Sexp.t -> variable
val hash_fold_variable : Base.Hash.state -> variable -> Base.Hash.state
val hash_variable : variable -> Base.Hash.hash_value
val compare_variable : variable -> variable -> int
type inductive = Names.inductive
val inductive_to_yojson : inductive -> Yojson.Safe.t
val sexp_of_inductive : inductive -> Sexplib0.Sexp.t
val inductive_of_sexp : Sexplib0.Sexp.t -> inductive
val hash_fold_inductive : Base.Hash.state -> inductive -> Base.Hash.state
val hash_inductive : inductive -> Base.Hash.hash_value
val compare_inductive : inductive -> inductive -> int
type constructor = Names.constructor
val constructor_to_yojson : constructor -> Yojson.Safe.t
val sexp_of_constructor : constructor -> Sexplib0.Sexp.t
val constructor_of_sexp : Sexplib0.Sexp.t -> constructor
val hash_fold_constructor : Base.Hash.state -> constructor -> Base.Hash.state
val hash_constructor : constructor -> Base.Hash.hash_value
val compare_constructor : constructor -> constructor -> int
module Projection : sig ... end
module GlobRef : SerType.SJHC with type t = Names.GlobRef.t
type lident = Names.lident
val lident_to_yojson : lident -> Yojson.Safe.t
val sexp_of_lident : lident -> Sexplib0.Sexp.t
val lident_of_sexp : Sexplib0.Sexp.t -> lident
val hash_fold_lident : Base.Hash.state -> lident -> Base.Hash.state
val hash_lident : lident -> Base.Hash.hash_value
val compare_lident : lident -> lident -> int
type lname = Names.lname
val lname_to_yojson : lname -> Yojson.Safe.t
val sexp_of_lname : lname -> Sexplib0.Sexp.t
val lname_of_sexp : Sexplib0.Sexp.t -> lname
val hash_fold_lname : Base.Hash.state -> lname -> Base.Hash.state
val hash_lname : lname -> Base.Hash.hash_value
val compare_lname : lname -> lname -> int
type lstring = Names.lstring
val lstring_to_yojson : lstring -> Yojson.Safe.t
val sexp_of_lstring : lstring -> Sexplib0.Sexp.t
val lstring_of_sexp : Sexplib0.Sexp.t -> lstring
val hash_fold_lstring : Base.Hash.state -> lstring -> Base.Hash.state
val hash_lstring : lstring -> Base.Hash.hash_value
val compare_lstring : lstring -> lstring -> int