coq-serapi 8.19.0+0.19.0 · OCaml Package

type hint_db_name = Hints.hint_db_name

val sexp_of_hint_db_name : hint_db_name -> Sexplib0.Sexp.t

val hint_db_name_of_sexp : Sexplib0.Sexp.t -> hint_db_name

val hint_db_name_to_yojson : hint_db_name -> Yojson.Safe.t

val hint_db_name_of_yojson : 
  Yojson.Safe.t ->
  hint_db_name Ppx_deriving_yojson_runtime.error_or

val hash_fold_hint_db_name : Base.Hash.state -> hint_db_name -> Base.Hash.state

val hash_hint_db_name : hint_db_name -> Base.Hash.hash_value

val compare_hint_db_name : hint_db_name -> hint_db_name -> int

type 'a hints_path_gen = 'a Hints.hints_path_gen

val sexp_of_hints_path_gen : 
  ('a -> Sexplib0.Sexp.t) ->
  'a hints_path_gen ->
  Sexplib0.Sexp.t

val hints_path_gen_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a hints_path_gen

val hints_path_gen_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a hints_path_gen ->
  Yojson.Safe.t

val hints_path_gen_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a hints_path_gen Ppx_deriving_yojson_runtime.error_or

val hash_fold_hints_path_gen : 
  (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a hints_path_gen ->
  Base.Hash.state

val compare_hints_path_gen : 
  ('a -> 'a -> int) ->
  'a hints_path_gen ->
  'a hints_path_gen ->
  int

type 'a hints_path_atom_gen = 'a Hints.hints_path_atom_gen

val sexp_of_hints_path_atom_gen : 
  ('a -> Sexplib0.Sexp.t) ->
  'a hints_path_atom_gen ->
  Sexplib0.Sexp.t

val hints_path_atom_gen_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a hints_path_atom_gen

val hints_path_atom_gen_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a hints_path_atom_gen ->
  Yojson.Safe.t

val hints_path_atom_gen_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a hints_path_atom_gen Ppx_deriving_yojson_runtime.error_or

val hash_fold_hints_path_atom_gen : 
  (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a hints_path_atom_gen ->
  Base.Hash.state

val compare_hints_path_atom_gen : 
  ('a -> 'a -> int) ->
  'a hints_path_atom_gen ->
  'a hints_path_atom_gen ->
  int

type hints_path = Hints.hints_path

val sexp_of_hints_path : hints_path -> Sexplib0.Sexp.t

val hints_path_of_sexp : Sexplib0.Sexp.t -> hints_path

val hints_path_to_yojson : hints_path -> Yojson.Safe.t

val hints_path_of_yojson : 
  Yojson.Safe.t ->
  hints_path Ppx_deriving_yojson_runtime.error_or

val hash_fold_hints_path : Base.Hash.state -> hints_path -> Base.Hash.state

val hash_hints_path : hints_path -> Base.Hash.hash_value

val compare_hints_path : hints_path -> hints_path -> int

type 'a hints_transparency_target = 'a Hints.hints_transparency_target

val sexp_of_hints_transparency_target : 
  ('a -> Sexplib0.Sexp.t) ->
  'a hints_transparency_target ->
  Sexplib0.Sexp.t

val hints_transparency_target_of_sexp : 
  (Sexplib0.Sexp.t -> 'a) ->
  Sexplib0.Sexp.t ->
  'a hints_transparency_target

val hints_transparency_target_to_yojson : 
  ('a -> Yojson.Safe.t) ->
  'a hints_transparency_target ->
  Yojson.Safe.t

val hints_transparency_target_of_yojson : 
  (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
  Yojson.Safe.t ->
  'a hints_transparency_target Ppx_deriving_yojson_runtime.error_or

val hash_fold_hints_transparency_target : 
  (Base.Hash.state -> 'a -> Base.Hash.state) ->
  Base.Hash.state ->
  'a hints_transparency_target ->
  Base.Hash.state

val compare_hints_transparency_target : 
  ('a -> 'a -> int) ->
  'a hints_transparency_target ->
  'a hints_transparency_target ->
  int

type hint_mode = Hints.hint_mode

val sexp_of_hint_mode : hint_mode -> Sexplib0.Sexp.t

val hint_mode_of_sexp : Sexplib0.Sexp.t -> hint_mode

val hint_mode_to_yojson : hint_mode -> Yojson.Safe.t

val hint_mode_of_yojson : 
  Yojson.Safe.t ->
  hint_mode Ppx_deriving_yojson_runtime.error_or

val hash_fold_hint_mode : Base.Hash.state -> hint_mode -> Base.Hash.state

val hash_hint_mode : hint_mode -> Base.Hash.hash_value

val compare_hint_mode : hint_mode -> hint_mode -> int

package coq-serapi