coq-serapi 8.15.0+0.15.4 · OCaml Package

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 Constant : SerType.SJHC with type t = Names.Constant.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 sexp_of_variable : variable -> Sexplib0.Sexp.t

val variable_of_sexp : Sexplib0.Sexp.t -> variable

val variable_to_yojson : variable -> Yojson.Safe.t

val variable_of_yojson : 
  Yojson.Safe.t ->
  variable Ppx_deriving_yojson_runtime.error_or

val hash_fold_variable : 
  Ppx_hash_lib.Std.Hash.state ->
  variable ->
  Ppx_hash_lib.Std.Hash.state

val hash_variable : variable -> Ppx_hash_lib.Std.Hash.hash_value

val compare_variable : variable -> variable -> int

type inductive = Names.inductive

val sexp_of_inductive : inductive -> Sexplib0.Sexp.t

val inductive_of_sexp : Sexplib0.Sexp.t -> inductive

val inductive_to_yojson : inductive -> Yojson.Safe.t

val inductive_of_yojson : 
  Yojson.Safe.t ->
  inductive Ppx_deriving_yojson_runtime.error_or

val hash_fold_inductive : 
  Ppx_hash_lib.Std.Hash.state ->
  inductive ->
  Ppx_hash_lib.Std.Hash.state

val hash_inductive : inductive -> Ppx_hash_lib.Std.Hash.hash_value

val compare_inductive : inductive -> inductive -> int

type constructor = Names.constructor

val sexp_of_constructor : constructor -> Sexplib0.Sexp.t

val constructor_of_sexp : Sexplib0.Sexp.t -> constructor

val constructor_to_yojson : constructor -> Yojson.Safe.t

val constructor_of_yojson : 
  Yojson.Safe.t ->
  constructor Ppx_deriving_yojson_runtime.error_or

val hash_fold_constructor : 
  Ppx_hash_lib.Std.Hash.state ->
  constructor ->
  Ppx_hash_lib.Std.Hash.state

val hash_constructor : constructor -> Ppx_hash_lib.Std.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 sexp_of_lident : lident -> Sexplib0.Sexp.t

val lident_of_sexp : Sexplib0.Sexp.t -> lident

val lident_to_yojson : lident -> Yojson.Safe.t

val lident_of_yojson : 
  Yojson.Safe.t ->
  lident Ppx_deriving_yojson_runtime.error_or

val hash_fold_lident : 
  Ppx_hash_lib.Std.Hash.state ->
  lident ->
  Ppx_hash_lib.Std.Hash.state

val hash_lident : lident -> Ppx_hash_lib.Std.Hash.hash_value

val compare_lident : lident -> lident -> int

type lname = Names.lname

val sexp_of_lname : lname -> Sexplib0.Sexp.t

val lname_of_sexp : Sexplib0.Sexp.t -> lname

val lname_to_yojson : lname -> Yojson.Safe.t

val lname_of_yojson : 
  Yojson.Safe.t ->
  lname Ppx_deriving_yojson_runtime.error_or

val hash_fold_lname : 
  Ppx_hash_lib.Std.Hash.state ->
  lname ->
  Ppx_hash_lib.Std.Hash.state

val hash_lname : lname -> Ppx_hash_lib.Std.Hash.hash_value

val compare_lname : lname -> lname -> int

type lstring = Names.lstring

val sexp_of_lstring : lstring -> Sexplib0.Sexp.t

val lstring_of_sexp : Sexplib0.Sexp.t -> lstring

val lstring_to_yojson : lstring -> Yojson.Safe.t

val lstring_of_yojson : 
  Yojson.Safe.t ->
  lstring Ppx_deriving_yojson_runtime.error_or

val hash_fold_lstring : 
  Ppx_hash_lib.Std.Hash.state ->
  lstring ->
  Ppx_hash_lib.Std.Hash.state

val hash_lstring : lstring -> Ppx_hash_lib.Std.Hash.hash_value

val compare_lstring : lstring -> lstring -> int

package coq-serapi