aboutsummaryrefslogtreecommitdiffhomepage
path: root/API/API.ml
blob: 2b7bbd561ba8d7487958bc7e5a79772829471f9b (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
(************************************************************************)
(*  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        *)
(************************************************************************)

module Ppvernac = Ppvernac
module Command = Command
module States = States
module Kindops = Kindops
module Coq_config = Coq_config
module Esubst = Esubst
module Evar = Evar
module Constrexpr = Constrexpr
module Libobject = Libobject
module Evd = Evd
module Libnames = Libnames
module Nameops = Nameops
module Topfmt = Topfmt
module Locus = Locus
module Locusops = Locusops
module Lemmas = Lemmas
module Clenv = Clenv
module Elimschemes = Elimschemes
module Classes = Classes
module Class_tactics = Class_tactics
module Eauto = Eauto
module Keys = Keys
module Vernac_classifier = Vernac_classifier
module Autorewrite = Autorewrite
module Redops = Redops
module Elim = Elim
module Geninterp = Geninterp
module Obligations = Obligations
module Retroknowledge = Retroknowledge
module Evar_refiner = Evar_refiner
module Hipattern = Hipattern
module Auto = Auto
module Hints = Hints
module Contradiction = Contradiction
module Tacticals = Tacticals
module Tactics = Tactics
module Inv = Inv
module Leminv = Leminv
module Equality = Equality
module Redexpr = Redexpr
module Pfedit = Pfedit
module Stm = Stm
module Stateid = Stateid
module Declaremods = Declaremods
module Miscops = Miscops
module Miscprint = Miscprint
module Genprint = Genprint
module Ppconstr = Ppconstr
module Pputils = Pputils
module Extend = Extend
module Logic = Logic
module Himsg = Himsg
module Tacred = Tacred
module Names = Names
module Indrec = Indrec
module Glob_ops = Glob_ops
module Constrexpr_ops = Constrexpr_ops
module Eqdecide = Eqdecide
module Genredexpr = Genredexpr
module Detyping = Detyping
module Tactypes = Tactypes
module ExplainErr = ExplainErr
module Printer = Printer
module Constrextern = Constrextern
module Locality = Locality
module Impargs = Impargs
module Termops = Termops
module Refiner = Refiner
module Ppextend = Ppextend
module Nametab = Nametab
module Vernacentries = Vernacentries
module Mltop = Mltop
module Goal = Goal
module Proof_global = Proof_global
module Proof = Proof
module Smartlocate = Smartlocate
module Dumpglob = Dumpglob
module Constrintern = Constrintern
module Topconstr = Topconstr
module Notation_ops = Notation_ops
module Patternops = Patternops
module Mod_typing = Mod_typing
module Modops = Modops
module Opaqueproof = Opaqueproof
module Ind_tables = Ind_tables
module Typeops = Typeops
module Inductive = Inductive
module Vars = Vars
module Reduction = Reduction
module Mod_subst = Mod_subst
module Sorts = Sorts
module Univ = Univ
module Constr = Constr
module CClosure = CClosure
module Type_errors = Type_errors
module Safe_typing = Safe_typing
module UGraph = UGraph
module Namegen = Namegen
module Ftactic = Ftactic
module UState = UState
module Proofview_monad = Proofview_monad
module Classops = Classops
module Global = Global
module Goptions = Goptions
module Lib = Lib
module Library = Library
module Summary = Summary
module Universes = Universes
module Declare = Declare
module Refine = Refine
module Find_subterm = Find_subterm
module Evar_kinds = Evar_kinds
module Decl_kinds = Decl_kinds
module Misctypes = Misctypes
module Pattern = Pattern
module Vernacexpr = Vernacexpr
module Search = Search
module Notation_term = Notation_term
module Reductionops = Reductionops
module Inductiveops = Inductiveops
module Recordops = Recordops
module Retyping = Retyping
module Typing = Typing
module Evarsolve = Evarsolve
module Constr_matching = Constr_matching
module Pretyping = Pretyping
module Evarconv = Evarconv
module Unification = Unification
module Typeclasses = Typeclasses
module Pretype_errors = Pretype_errors
module Notation = Notation
module Declarations = Declarations
module Declareops = Declareops
module Globnames = Globnames
module Environ = Environ
module Term = Term
module Coqlib = Coqlib
module Glob_term = Glob_term
module Context = Context
module Stdarg = Stdarg
module Tacmach = Tacmach
module Proofview = Proofview
module Evarutil = Evarutil
module EConstr = EConstr

module Prelude =
  struct
    type global_reference = Globnames.global_reference
    type metavariable = int
    type meta_value_map = (metavariable * Constr.constr) list
    type named_context_val = Environ.named_context_val
    type conv_pb = Reduction.conv_pb =
      | CONV
      | CUMUL
    type constr = Constr.constr
    type types = Constr.types
    type evar = Constr.existential_key
    type 'constr pexistential = 'constr Constr.pexistential
    type env = Environ.env
    type evar_map = Evd.evar_map
    type rigid = Evd.rigid =
               | UnivRigid
               | UnivFlexible of bool
    type reference = Libnames.reference =
      | Qualid of Libnames.qualid Loc.located
      | Ident of Names.Id.t Loc.located
  end

(* NOTE: It does not make sense to replace the following "module expression"
   simply with "module Proof_type = Proof_type" because
   there is only "kernel/entries.mli";
   there is no "kernel/entries.ml" file *)
module Entries =
  struct
    type mutual_inductive_entry = Entries.mutual_inductive_entry
    type inline = int option
    type 'a proof_output = Constr.constr Univ.in_universe_context_set * 'a
    type 'a const_entry_body = 'a proof_output Future.computation
    type 'a definition_entry = 'a Entries.definition_entry =
                                 { const_entry_body   : 'a const_entry_body;
                                   const_entry_secctx : Context.Named.t option;
                                   const_entry_feedback : Stateid.t option;
                                   const_entry_type        : Term.types option;
                                   const_entry_polymorphic : bool;
                                   const_entry_universes   : Univ.universe_context;
                                   const_entry_opaque      : bool;
                                   const_entry_inline_code : bool }
    type parameter_entry = Entries.parameter_entry
    type projection_entry = Entries.projection_entry
    type 'a constant_entry = 'a Entries.constant_entry =
                           | DefinitionEntry of 'a definition_entry
                           | ParameterEntry of parameter_entry
                           | ProjectionEntry of projection_entry
  end

(* NOTE: It does not make sense to replace the following "module expression"
   simply with "module Proof_type = Proof_type" because
   there is only "proofs/proof_type.mli";
   there is no "proofs/proof_type.ml" file *)
module Proof_type =
  struct
    type goal = Goal.goal
    type tactic = goal Evd.sigma -> goal list Evd.sigma
    type rule = Proof_type.prim_rule =
      | Cut of bool * bool * Names.Id.t * Term.types
      | Refine of Term.constr
  end