coq-serapi 8.17.0+0.17.2 · OCaml Package

type side = Extend.side

val side_of_sexp : Sexplib.Sexp.t -> side

val sexp_of_side : side -> Sexplib.Sexp.t

type production_position = Extend.production_position

val production_position_of_sexp : Sexplib.Sexp.t -> production_position

val sexp_of_production_position : production_position -> Sexplib.Sexp.t

type production_level = Extend.production_level

val sexp_of_production_level : production_level -> Sexplib0.Sexp.t

val production_level_of_sexp : Sexplib0.Sexp.t -> production_level

val production_level_to_yojson : production_level -> Yojson.Safe.t

val production_level_of_yojson : 
  Yojson.Safe.t ->
  production_level Ppx_deriving_yojson_runtime.error_or

val hash_fold_production_level : 
  Ppx_hash_lib.Std.Hash.state ->
  production_level ->
  Ppx_hash_lib.Std.Hash.state

val hash_production_level : 
  production_level ->
  Ppx_hash_lib.Std.Hash.hash_value

val compare_production_level : production_level -> production_level -> int

type binder_entry_kind = Extend.binder_entry_kind

val binder_entry_kind_of_sexp : Sexplib.Sexp.t -> binder_entry_kind

val sexp_of_binder_entry_kind : binder_entry_kind -> Sexplib.Sexp.t

type 'lev constr_entry_key_gen = 'lev Extend.constr_entry_key_gen

val constr_entry_key_gen_of_sexp : 
  (Sexplib.Sexp.t -> 'lev) ->
  Sexplib.Sexp.t ->
  'lev constr_entry_key_gen

val sexp_of_constr_entry_key_gen : 
  ('lev -> Sexplib.Sexp.t) ->
  'lev constr_entry_key_gen ->
  Sexplib.Sexp.t

type constr_entry_key = Extend.constr_entry_key

val constr_entry_key_of_sexp : Sexplib.Sexp.t -> constr_entry_key

val sexp_of_constr_entry_key : constr_entry_key -> Sexplib.Sexp.t

type constr_prod_entry_key = Extend.constr_prod_entry_key

val constr_prod_entry_key_of_sexp : Sexplib.Sexp.t -> constr_prod_entry_key

val sexp_of_constr_prod_entry_key : constr_prod_entry_key -> Sexplib.Sexp.t

type simple_constr_prod_entry_key = Extend.simple_constr_prod_entry_key

val sexp_of_simple_constr_prod_entry_key : 
  simple_constr_prod_entry_key ->
  Sexplib0.Sexp.t

val simple_constr_prod_entry_key_of_sexp : 
  Sexplib0.Sexp.t ->
  simple_constr_prod_entry_key

val simple_constr_prod_entry_key_to_yojson : 
  simple_constr_prod_entry_key ->
  Yojson.Safe.t

val simple_constr_prod_entry_key_of_yojson : 
  Yojson.Safe.t ->
  simple_constr_prod_entry_key Ppx_deriving_yojson_runtime.error_or

val hash_fold_simple_constr_prod_entry_key : 
  Ppx_hash_lib.Std.Hash.state ->
  simple_constr_prod_entry_key ->
  Ppx_hash_lib.Std.Hash.state

val hash_simple_constr_prod_entry_key : 
  simple_constr_prod_entry_key ->
  Ppx_hash_lib.Std.Hash.hash_value

val compare_simple_constr_prod_entry_key : 
  simple_constr_prod_entry_key ->
  simple_constr_prod_entry_key ->
  int

package coq-serapi