aboutsummaryrefslogtreecommitdiffhomepage
path: root/API/API.ml
blob: 378c03ee4fa14e17fe94e40b1d1b1919db5fc76f (plain)
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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Warning, this file respects the dependency order established in Coq.

   To see such order issue the comand:

   ```
   bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link
   ```
 *)

(******************************************************************************)
(* config                                                                     *)
(******************************************************************************)
module Coq_config = Coq_config

(******************************************************************************)
(* Kernel *)
(******************************************************************************)
(* "mli" files *)
module Declarations = Declarations
module Entries = Entries

module Names = Names
(* module Uint31 *)
module Univ = Univ
module UGraph = UGraph
module Esubst = Esubst
module Sorts = Sorts
module Evar = Evar
module Constr = Constr
module Context = Context
module Vars = Vars
module Term = Term
module Mod_subst = Mod_subst
module Cbytecodes = Cbytecodes
(* module Copcodes *)
module Cemitcodes = Cemitcodes
(* module Nativevalues *)
(* module CPrimitives *)
module Opaqueproof = Opaqueproof
module Declareops = Declareops
module Retroknowledge = Retroknowledge
module Conv_oracle = Conv_oracle
(* module Pre_env *)
(* module Cbytegen *)
(* module Nativelambda *)
(* module Nativecode *)
(* module Nativelib *)
module Environ = Environ
module CClosure = CClosure
module Reduction = Reduction
(* module Nativeconv *)
module Type_errors = Type_errors
module Modops = Modops
module Inductive = Inductive
module Typeops = Typeops
(* module Indtypes *)
(* module Cooking *)
(* module Term_typing *)
(* module Subtyping *)
module Mod_typing = Mod_typing
(* module Nativelibrary *)
module Safe_typing = Safe_typing
(* module Vm *)
(* module Csymtable *)
(* module Vconv *)

(******************************************************************************)
(* Intf                                                                       *)
(******************************************************************************)
module Constrexpr = Constrexpr
module Locus = Locus
module Glob_term = Glob_term
module Extend = Extend
module Misctypes = Misctypes
module Pattern = Pattern
module Decl_kinds = Decl_kinds
module Vernacexpr = Vernacexpr
module Notation_term = Notation_term
module Evar_kinds = Evar_kinds
module Genredexpr = Genredexpr

(******************************************************************************)
(* Library *)
(******************************************************************************)
module Univops = Univops
module Nameops = Nameops
module Libnames = Libnames
module Globnames = Globnames
module Libobject = Libobject
module Summary = Summary
module Nametab = Nametab
module Global = Global
module Lib = Lib
module Declaremods = Declaremods
(* module Loadpath *)
module Library = Library
module States = States
module Kindops = Kindops
(* module Dischargedhypsmap *)
module Goptions = Goptions
(* module Decls *)
(* module Heads *)
module Keys = Keys
module Coqlib = Coqlib

(******************************************************************************)
(* Engine                                                                     *)
(******************************************************************************)
(* module Logic_monad *)
module Universes = Universes
module UState = UState
module Evd = Evd
module EConstr = EConstr
module Namegen = Namegen
module Termops = Termops
module Proofview_monad = Proofview_monad
module Evarutil = Evarutil
module Proofview = Proofview
module Ftactic = Ftactic
module Geninterp = Geninterp

(******************************************************************************)
(* Pretyping                                                                  *)
(******************************************************************************)
module Ltac_pretype = Ltac_pretype
module Locusops = Locusops
module Pretype_errors = Pretype_errors
module Reductionops = Reductionops
module Inductiveops = Inductiveops
(* module Vnorm *)
(* module Arguments_renaming *)
module Impargs = Impargs
(* module Nativenorm *)
module Retyping = Retyping
(* module Cbv *)
module Find_subterm = Find_subterm
(* module Evardefine *)
module Evarsolve = Evarsolve
module Recordops = Recordops
module Evarconv = Evarconv
module Typing = Typing
module Miscops = Miscops
module Glob_ops = Glob_ops
module Redops = Redops
module Patternops = Patternops
module Constr_matching = Constr_matching
module Tacred = Tacred
module Typeclasses = Typeclasses
module Classops = Classops
(* module Program *)
(* module Coercion *)
module Detyping = Detyping
module Indrec = Indrec
(* module Cases *)
module Pretyping = Pretyping
module Unification = Unification
module Univdecls = Univdecls
(******************************************************************************)
(* interp                                                                     *)
(******************************************************************************)
module Tactypes = Tactypes
module Stdarg = Stdarg
module Genintern = Genintern
module Constrexpr_ops = Constrexpr_ops
module Notation_ops = Notation_ops
module Notation = Notation
module Dumpglob = Dumpglob
(* module Syntax_def *)
module Smartlocate = Smartlocate
module Topconstr = Topconstr
(* module Reserve *)
(* module Implicit_quantifiers *)
module Constrintern = Constrintern
(* module Modintern *)
module Constrextern = Constrextern
(* module Discharge *)
module Declare = Declare

(******************************************************************************)
(* Proofs                                                                     *)
(******************************************************************************)
module Miscprint = Miscprint
module Goal = Goal
module Evar_refiner = Evar_refiner
(* module Proof_using *)
module Proof_type = Proof_type
module Logic = Logic
module Refine = Refine
module Proof = Proof
module Proof_bullet = Proof_bullet
module Proof_global = Proof_global
module Redexpr = Redexpr
module Refiner = Refiner
module Tacmach = Tacmach
module Pfedit = Pfedit
module Clenv = Clenv
(* module Clenvtac *)
(* "mli" file *)

(******************************************************************************)
(* Printing                                                                   *)
(******************************************************************************)
module Genprint = Genprint
module Pputils = Pputils
module Ppconstr = Ppconstr
module Printer = Printer
(* module Printmod *)
module Prettyp = Prettyp
module Ppvernac = Ppvernac

(******************************************************************************)
(* Parsing                                                                    *)
(******************************************************************************)
module Tok = Tok
module CLexer = CLexer
module Pcoq = Pcoq
module Egramml = Egramml
(* Egramcoq *)

module G_vernac = G_vernac
module G_proofs = G_proofs

(******************************************************************************)
(* Tactics                                                                    *)
(******************************************************************************)
(* module Dnet *)
(* module Dn *)
(* module Btermdn *)
module Tacticals = Tacticals
module Hipattern = Hipattern
module Ind_tables = Ind_tables
(* module Eqschemes *)
module Elimschemes = Elimschemes
module Tactics = Tactics
module Elim = Elim
module Equality = Equality
module Contradiction = Contradiction
module Inv = Inv
module Leminv = Leminv
module Hints = Hints
module Auto = Auto
module Eauto = Eauto
module Class_tactics = Class_tactics
(* module Term_dnet *)
module Eqdecide = Eqdecide
module Autorewrite = Autorewrite

(******************************************************************************)
(* Vernac                                                                     *)
(******************************************************************************)
(* module Vernacprop *)
module Lemmas = Lemmas
module Himsg = Himsg
module ExplainErr = ExplainErr
(* module Class *)
module Locality = Locality
module Metasyntax = Metasyntax
(* module Auto_ind_decl *)
module Search = Search
(* module Indschemes *)
module Obligations = Obligations
module Command = Command
module Classes = Classes
(* module Record *)
(* module Assumptions *)
module Vernacstate = Vernacstate
module Vernacinterp = Vernacinterp
module Mltop = Mltop
module Topfmt = Topfmt
module Vernacentries = Vernacentries

(******************************************************************************)
(* Stm                                                                        *)
(******************************************************************************)
module Vernac_classifier = Vernac_classifier
module Stm = Stm