coq-serapi 8.10.0+0.7.1 · OCaml Package

coq-serapi

module Id : sig ... end

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

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

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

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

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

module MPmap : Ser_cMap.ExtS with type key = ModPath.t

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

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

module Cmap : Ser_cMap.ExtS with type key = Constant.t

module Cmap_env : Ser_cMap.ExtS with type key = Constant.t

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

module Mindmap : Ser_cMap.ExtS with type key = MutInd.t

module Mindmap_env : Ser_cMap.ExtS with type key = MutInd.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

type inductive = Names.inductive

type constructor = Names.constructor

module Projection : sig ... end

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

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 inductive_of_yojson : Yojson.Safe.t -> (inductive, string) Result.result

val inductive_to_yojson : inductive -> Yojson.Safe.t

val constructor_of_sexp : Sexplib.Sexp.t -> constructor

val sexp_of_constructor : constructor -> Sexplib.Sexp.t

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

val constructor_to_yojson : constructor -> Yojson.Safe.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

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

val lident_to_yojson : lident -> Yojson.Safe.t

type lname = Names.lname

val lname_of_sexp : Sexplib.Sexp.t -> lname

val sexp_of_lname : lname -> Sexplib.Sexp.t

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

val lname_to_yojson : lname -> Yojson.Safe.t

type lstring = Names.lstring

val lstring_of_sexp : Sexplib.Sexp.t -> lstring

val sexp_of_lstring : lstring -> Sexplib.Sexp.t

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

val lstring_to_yojson : lstring -> Yojson.Safe.t

package coq-serapi