package coq-serapi

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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] *)
OCaml

Innovation. Community. Security.