package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.3.9.0.tbz
sha256=8776582dddfe768623870cf540ff6ba1e96a44a36e85db18ab93d238d640f92a
sha512=2837889bf99bfe715bd0e752782211a76a14aac71ed37a4fb784f4f0abe338352c9c6d8caa37daf79c036997add1cb306c523f793625b38709f3b5e245380223
doc/src/coq-lsp.serlib/ser_entries.ml.html
Source file ser_entries.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 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (************************************************************************) (* SerAPI: Coq interaction protocol with bidirectional serialization *) (************************************************************************) (* Copyright 2016-2019 MINES ParisTech -- License LGPL 2.1+ *) (* Copyright 2019-2023 Inria -- License LGPL 2.1+ *) (* Written by: Emilio J. Gallego Arias and others *) (************************************************************************) open Sexplib.Conv module Stateid = Ser_stateid module Future = Ser_future module Names = Ser_names module Univ = Ser_univ module UVars = Ser_uvars module Constr = Ser_constr module Declarations = Ser_declarations module CPrimitives = Ser_cPrimitives (* type local_entry = * [%import: Entries.local_entry] * [@@deriving sexp] *) (* type inductive_universes = * [%import: Entries.inductive_universes] * [@@deriving sexp] *) type universes_entry = [%import: Entries.universes_entry] [@@deriving sexp] type 'a in_universes_entry = [%import: 'a Entries.in_universes_entry] [@@deriving sexp] type one_inductive_entry = [%import: Entries.one_inductive_entry] [@@deriving sexp] type variance_entry = [%import: Entries.variance_entry] [@@deriving sexp] (* type mutual_inductive_entry = * [%import: Entries.mutual_inductive_entry] * [@@deriving sexp] *) type 'a proof_output = [%import: 'a Entries.proof_output] [@@deriving sexp] (* type 'a const_entry_body = * [%import: 'a Entries.const_entry_body] * [@@deriving sexp] *) (* type constant_universes_entry = * [%import: Entries.constant_universes_entry] * [@@deriving sexp] *) (* type 'a in_constant_universes_entry = * [%import: 'a Entries.in_constant_universes_entry] * [@@deriving sexp] *) type definition_entry = [%import: Entries.definition_entry] [@@deriving sexp] type section_def_entry = [%import: Entries.section_def_entry] [@@deriving sexp] type inline = [%import: Entries.inline] [@@deriving sexp] type 'a opaque_entry = [%import: 'a Entries.opaque_entry] [@@deriving sexp] type parameter_entry = [%import: Entries.parameter_entry] [@@deriving sexp] type primitive_entry = [%import: Entries.primitive_entry] [@@deriving sexp] type symbol_entry = [%import: Entries.symbol_entry] [@@deriving sexp] type constant_entry = [%import: Entries.constant_entry] [@@deriving sexp] type module_struct_entry = [%import: Entries.module_struct_entry] [@@deriving sexp] type module_params_entry = [%import: Entries.module_params_entry] [@@deriving sexp] type module_entry = [%import: Entries.module_entry] [@@deriving sexp] type module_type_entry = [%import: Entries.module_type_entry] [@@deriving sexp] (* type seff_env = * [%import: Entries.seff_env] * [@@deriving sexp] *) (* type side_effect_role = * [%import: Entries.side_effect_role] * [@@deriving sexp] *) (* type side_eff = * [%import: Entries.side_eff] * [@@deriving sexp] *)