Ser_names (p.coq-serapi.8.13.0+0.13.0.doc.coq-serapi.serlib.Serlib.Ser

Sourcemodule Id : sig ... end

Sourcemodule Name : SerType.SJ with type t = Names.Name.t

Sourcemodule DirPath : SerType.SJ with type t = Names.DirPath.t

module DPmap : 
  Ser_cMap.ExtS with type key = DirPath.t and type 'a t = 'a Names.DPmap.t

Sourcemodule Label : SerType.S with type t = Names.Label.t

Sourcemodule MBId : SerType.S with type t = Names.MBId.t

Sourcemodule ModPath : SerType.S with type t = Names.ModPath.t

Source

module MPmap : 
  Ser_cMap.ExtS with type key = ModPath.t and type 'a t = 'a Names.MPmap.t

Sourcemodule KerName : SerType.S with type t = Names.KerName.t

Sourcemodule Constant : SerType.SJ with type t = Names.Constant.t

Source

module Cmap : 
  Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap.t

Source

module Cmap_env : 
  Ser_cMap.ExtS with type key = Constant.t and type 'a t = 'a Names.Cmap_env.t

Sourcemodule MutInd : SerType.S with type t = Names.MutInd.t

Source

module Mindmap : 
  Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap.t

Source

module Mindmap_env : 
  Ser_cMap.ExtS with type key = MutInd.t and type 'a t = 'a Names.Mindmap_env.t

Sourcetype 'a tableKey = 'a Names.tableKey

Sourceval tableKey_of_sexp : (Sexplib.Sexp.t -> 'a) -> Sexplib.Sexp.t -> 'a tableKey

Sourceval sexp_of_tableKey : ('a -> Sexplib.Sexp.t) -> 'a tableKey -> Sexplib.Sexp.t

Sourcetype variable = Names.variable

Sourcetype inductive = Names.inductive

Sourcetype constructor = Names.constructor

Sourcemodule Projection : sig ... end

Sourcemodule GlobRef : SerType.SJ with type t = Names.GlobRef.t

Sourceval variable_of_sexp : Sexplib.Sexp.t -> variable

Sourceval sexp_of_variable : variable -> Sexplib.Sexp.t

Sourceval inductive_of_sexp : Sexplib.Sexp.t -> inductive

Sourceval sexp_of_inductive : inductive -> Sexplib.Sexp.t

Sourceval inductive_of_yojson : Yojson.Safe.t -> (inductive, string) Result.result

Sourceval inductive_to_yojson : inductive -> Yojson.Safe.t

Sourceval constructor_of_sexp : Sexplib.Sexp.t -> constructor

Sourceval sexp_of_constructor : constructor -> Sexplib.Sexp.t

Source

val constructor_of_yojson : 
  Yojson.Safe.t ->
  (constructor, string) Result.result

Sourceval constructor_to_yojson : constructor -> Yojson.Safe.t

Sourcetype evaluable_global_reference = Names.evaluable_global_reference

Source

val evaluable_global_reference_of_sexp : 
  Sexplib.Sexp.t ->
  evaluable_global_reference

Source

val sexp_of_evaluable_global_reference : 
  evaluable_global_reference ->
  Sexplib.Sexp.t

Sourcetype lident = Names.lident

Sourceval lident_of_sexp : Sexplib.Sexp.t -> lident

Sourceval sexp_of_lident : lident -> Sexplib.Sexp.t

Sourceval lident_of_yojson : Yojson.Safe.t -> (lident, string) Result.result

Sourceval lident_to_yojson : lident -> Yojson.Safe.t

Sourcetype lname = Names.lname

Sourceval lname_of_sexp : Sexplib.Sexp.t -> lname

Sourceval sexp_of_lname : lname -> Sexplib.Sexp.t

Sourceval lname_of_yojson : Yojson.Safe.t -> (lname, string) Result.result

Sourceval lname_to_yojson : lname -> Yojson.Safe.t

Sourcetype lstring = Names.lstring

Sourceval lstring_of_sexp : Sexplib.Sexp.t -> lstring

Sourceval sexp_of_lstring : lstring -> Sexplib.Sexp.t

Sourceval lstring_of_yojson : Yojson.Safe.t -> (lstring, string) Result.result

Sourceval lstring_to_yojson : lstring -> Yojson.Safe.t