package coq-serapi

  1. Overview
  2. Docs
package coq-serapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Names = Ser_names
module Mod_subst = Ser_mod_subst
module CString : sig ... end
type _open_filter =
  1. | Unfiltered
  2. | Filtered of CString.Pred.t
val _open_filter_of_sexp : Sexplib0.Sexp.t -> _open_filter
val sexp_of__open_filter : _open_filter -> Sexplib0.Sexp.t
val _t_put : 'a -> 'b
val _t_get : 'a -> 'b
type open_filter = Libobject.open_filter
val open_filter_of_sexp : Sexplib0.Sexp.t -> 'a
val sexp_of_open_filter : 'a -> Sexplib0.Sexp.t
module Dyn : sig ... end
type obj = Dyn.t
val obj_of_sexp : Sexplib0.Sexp.t -> obj
val sexp_of_obj : obj -> Sexplib0.Sexp.t
type algebraic_objects = Libobject.algebraic_objects =
  1. | Objs of t list
  2. | Ref of Names.ModPath.t * Mod_subst.substitution
and t = Libobject.t =
  1. | ModuleObject of Names.Id.t * substitutive_objects
  2. | ModuleTypeObject of Names.Id.t * substitutive_objects
  3. | IncludeObject of algebraic_objects
  4. | KeepObject of Names.Id.t * t list
  5. | ExportObject of {
    1. mpl : (open_filter * Names.ModPath.t) list;
    }
  6. | AtomicObject of obj
and substitutive_objects = Names.MBId.t list * algebraic_objects
val algebraic_objects_of_sexp : Sexplib0.Sexp.t -> algebraic_objects
val t_of_sexp : Sexplib0.Sexp.t -> t
val substitutive_objects_of_sexp : Sexplib0.Sexp.t -> substitutive_objects
val sexp_of_algebraic_objects : algebraic_objects -> Sexplib0.Sexp.t
val sexp_of_t : t -> Sexplib0.Sexp.t
val sexp_of_substitutive_objects : substitutive_objects -> Sexplib0.Sexp.t
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct