package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.2.0.8.20.tbz
sha256=bcb9a4c3219aed47ffbfd7c8ea7a2f374140d8cdb76079927548f49c7e3576a9
sha512=945c0010b4952e41055cb7e35175d400e5c126dc340dd1c0ab53321605cd0d9539af6693a794cb81a9dec0385d0880d4417dae923b6d19c9b62913766a185d8c
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] *)