coq-serapi.serlib_extra
Serlib_extra.Ser_coqargs
coq-serapi.coq
coq-serapi.serapi_v8_14
coq-serapi.serlib
coq-serapi.sertop_v8_12
serlib_btauto
serlib_cc
serlib_extraction
serlib_firstorder
serlib_funind
serlib_ltac
serlib_ltac2
serlib_micromega
serlib_micromega_core
serlib_number_string_notation_plugin
serlib_ring
serlib_ssr
serlib_ssrmatching
serlib_tauto
serlib_zify
module Names = Serlib.Ser_names
module Lib = Serlib.Ser_lib
type top = Coqargs.top =
| TopLogical of Names.DirPath.t
| TopPhysical of string
val top_of_sexp : Sexplib0.Sexp.t -> top
val sexp_of_top : top -> Sexplib0.Sexp.t
type require_injection = Coqargs.require_injection = {
lib : string;
prefix : string option;
export : Lib.export_flag option;
}
val require_injection_of_sexp : Sexplib0.Sexp.t -> require_injection
val sexp_of_require_injection : require_injection -> Sexplib0.Sexp.t