blob: 1410cc7a0b3ab41974605442509e24e280f8ba17 (
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
|
Coq_config
Hook
CMap
Int
Option
Store
Exninfo
Backtrace
IStream
Pp_control
Loc
Compat
Flags
Pp
Segmenttree
Unicodetable
Unicode
Errors
Hashset
Hashcons
CObj
CList
CString
CArray
CStack
Util
Bigint
Dyn
CUnix
System
Envars
Profile
Explore
Predicate
Rtree
Heap
Dnet
Genarg
Stateid
Ephemeron
Future
RemoteCounter
Names
Univ
Esubst
Sorts
Evar
Constr
Context
Vars
Term
Mod_subst
Cbytecodes
Copcodes
Cemitcodes
Nativevalues
Future
Lazyconstr
Declareops
Retroknowledge
Conv_oracle
Pre_env
Nativelambda
Nativecode
Nativelib
Cbytegen
Environ
Closure
Reduction
Nativeconv
Type_errors
Modops
Inductive
Typeops
Indtypes
Cooking
Term_typing
Subtyping
Mod_typing
Nativelibrary
Safe_typing
Summary
Nameops
Libnames
Globnames
Global
Nametab
Libobject
Lib
Loadpath
Goptions
Decls
Heads
Assumptions
Locusops
Miscops
Termops
Namegen
Evd
Glob_ops
Redops
Reductionops
Inductiveops
Retyping
Cbv
Pretype_errors
Evarutil
Evarsolve
Term_dnet
Recordops
Evarconv
Arguments_renaming
Typing
Patternops
Matching
Tacred
Classops
Typeclasses_errors
Typeclasses
Detyping
Indrec
Program
Coercion
Unification
Cases
Pretyping
Declaremods
Library
States
Genprint
Tok
Lexer
Ppextend
Pputils
Stdarg
Constrarg
Constrexpr_ops
Notation_ops
Topconstr
Notation
Dumpglob
Reserve
Impargs
Syntax_def
Implicit_quantifiers
Smartlocate
Constrintern
Modintern
Constrextern
Proof_type
Goal
Logic
Refiner
Clenv
Evar_refiner
Proof_errors
Proofview_gen
Proofview_monad
Proofview
Proof
Proof_global
Pfedit
Tactic_debug
Decl_mode
Ppconstr
Pcoq
Printer
Pptactic
Ppdecl_proof
Egramml
Egramcoq
Himsg
Cerrors
Locality
Vernacinterp
Top_printers
|
