package coq-serapi
Serialization library and protocol for machine interaction with the Coq proof assistant
Install
Dune Dependency
Authors
Maintainers
Sources
coq-serapi-8.18.0.0.18.2.tbz
sha256=0fcf20002a6856b6d2485dcb55d388558dd771a8dcb99f5c614b8f5519f90801
sha512=45fa6873a65160624952de89d51ab3c44522c3485e945974e5fe97bc3c5214fa7955cd993f69bc1b87b3cfce77fde81b39ec9a43263ab4a14513a13b7c6ded92
doc/src/coq-serapi.serlib/ser_lib.ml.html
Source file ser_lib.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (************************************************************************) (* Coq serialization API/Plugin *) (* Copyright 2016-2019 MINES ParisTech *) (* Copyright 2019-2022 Inria *) (************************************************************************) open Sexplib.Std module Nametab = Ser_nametab module Libobject = Ser_libobject module Summary = Ser_summary type is_type = [%import: Lib.is_type] [@@deriving sexp] type export_flag = [%import: Lib.export_flag] [@@deriving sexp] type export = [%import: Lib.export] [@@deriving sexp] type 'a node = [%import: 'a Lib.node] [@@deriving sexp] type 'a library_segment = [%import: 'a Lib.library_segment] [@@deriving sexp]