dev/printers.mllib


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

Coq_config

Terminal
Hook
Canary
Hashset
Hashcons
CSet
CMap
Int
Dyn
HMap
Option
Store
Exninfo
Backtrace
IStream
Pp_control
Loc
CList
CString
Tok
Compat
Flags
Control
Loc
Serialize
Stateid
Feedback
Pp
Segmenttree
Unicodetable
Unicode
CObj
CArray
CStack
Util
Ppstyle
Errors
Bigint
CUnix
System
Envars
Aux_file
Profile
Explore
Predicate
Rtree
Heap
Genarg
Stateid
CEphemeron
Future
RemoteCounter
Monad

Names
Univ
UGraph
Esubst
Uint31
Sorts
Evar
Constr
Context
Vars
Term
Mod_subst
Cbytecodes
Copcodes
Cemitcodes
Nativevalues
Primitives
Nativeinstr
Future
Opaqueproof
Declareops
Retroknowledge
Conv_oracle
Pre_env
Nativelambda
Nativecode
Nativelib
Cbytegen
Environ
Closure
Reduction
Nativeconv
Type_errors
Modops
Inductive
Typeops
Fast_typeops
Indtypes
Cooking
Term_typing
Subtyping
Mod_typing
Nativelibrary
Safe_typing
Unionfind

Summary
Nameops
Libnames
Globnames
Global
Nametab
Libobject
Lib
Loadpath
Goptions
Decls
Heads
Keys
Locusops
Miscops
Universes
Termops
Namegen
UState
Evd
Sigma
Glob_ops
Redops
Pretype_errors
Evarutil
Reductionops
Inductiveops
Arguments_renaming
Nativenorm
Retyping
Cbv

Evardefine
Evarsolve
Recordops
Evarconv
Typing
Patternops
Constr_matching
Find_subterm
Tacred
Classops
Typeclasses_errors
Logic_monad
Proofview_monad
Proofview
Typeclasses
Detyping
Indrec
Program
Coercion
Cases
Pretyping
Unification
Declaremods
Library
States

Genprint
Lexer
Ppextend
Pputils
Ppannotation
Stdarg
Constrarg
Constrexpr_ops
Genintern
Notation_ops
Notation
Dumpglob
Syntax_def
Smartlocate
Topconstr
Reserve
Impargs
Implicit_quantifiers
Constrintern
Modintern
Constrextern
Goal
Miscprint
Logic
Refiner
Clenv
Evar_refiner
Proof_errors
Refine
Proof
Proof_global
Pfedit
Decl_mode
Ppconstr
Entry
Pcoq
Printer
Pptactic
Ppdecl_proof
Egramml
Egramcoq
Tacsubst
Trie
Dn
Btermdn
Hints
Himsg
Cerrors
Locality
Assumptions
Vernacinterp
Dischargedhypsmap
Discharge
Declare
Ind_tables
Top_printers