-
Notifications
You must be signed in to change notification settings - Fork 0
/
_CoqProject
235 lines (223 loc) · 7.86 KB
/
_CoqProject
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
-Q src/burrow Burrow
src/burrow/assoc_comm.v
src/burrow/building.v
src/burrow/exchange_proof.v
src/burrow/exchanges.v
src/burrow/fresh.v
src/burrow/gmap_utils.v
src/burrow/indexing.v
src/burrow/live_rec.v
src/burrow/maxltunit.v
src/burrow/parity.v
src/burrow/locations.v
src/burrow/ra.v
src/burrow/relive.v
src/burrow/resource_proofs.v
src/burrow/trees.v
src/burrow/tactics.v
src/burrow/tpcms.v
src/burrow/updog.v
-Q src/tpcms Tpcms
src/tpcms/gmap.v
src/tpcms/auth_frag.v
src/tpcms/heap.v
src/tpcms/rwlock.v
src/tpcms/hash_table.v
-Q src/lang BurrowLang
src/lang/adequacy.v
src/lang/class_instances.v
src/lang/heap_ra.v
src/lang/lang.v
src/lang/notation.v
src/lang/primitive_laws.v
src/lang/proofmode.v
src/lang/simp.v
src/lang/tactics.v
-Q src/examples Examples
src/examples/rwlock.v
src/examples/seqs.v
src/examples/hash_table.v
-arg -w -arg -ssr-search-moved
-arg -w -arg -deprecated-hint-without-locality
-arg -w -arg -deprecated-instance-without-locality
-arg -w -arg -deprecated-hint-rewrite-without-locality
-arg -w -arg +deprecated-tactic-notation
# Iris-disabled warnings
-arg -w -arg -notation-overridden,-redundant-canonical-projection
-Q external/stdpp/theories stdpp
-Q external/iris/iris iris
-Q external/coq-tricks coq_tricks
-Q external/cpdt cpdt
external/coq-tricks/Deex.v
external/cpdt/CpdtTactics.v
external/iris/iris/prelude/options.v
external/iris/iris/prelude/prelude.v
external/iris/iris/algebra/monoid.v
external/iris/iris/algebra/cmra.v
external/iris/iris/algebra/big_op.v
external/iris/iris/algebra/cmra_big_op.v
external/iris/iris/algebra/sts.v
external/iris/iris/algebra/numbers.v
external/iris/iris/algebra/view.v
external/iris/iris/algebra/auth.v
external/iris/iris/algebra/gmap.v
external/iris/iris/algebra/ofe.v
external/iris/iris/algebra/cofe_solver.v
external/iris/iris/algebra/agree.v
external/iris/iris/algebra/excl.v
external/iris/iris/algebra/functions.v
external/iris/iris/algebra/frac.v
external/iris/iris/algebra/dfrac.v
external/iris/iris/algebra/csum.v
external/iris/iris/algebra/list.v
external/iris/iris/algebra/vector.v
external/iris/iris/algebra/updates.v
external/iris/iris/algebra/local_updates.v
external/iris/iris/algebra/gset.v
external/iris/iris/algebra/gmultiset.v
external/iris/iris/algebra/coPset.v
external/iris/iris/algebra/proofmode_classes.v
external/iris/iris/algebra/ufrac.v
external/iris/iris/algebra/reservation_map.v
external/iris/iris/algebra/dyn_reservation_map.v
external/iris/iris/algebra/max_prefix_list.v
external/iris/iris/algebra/lib/excl_auth.v
external/iris/iris/algebra/lib/frac_auth.v
external/iris/iris/algebra/lib/ufrac_auth.v
external/iris/iris/algebra/lib/frac_agree.v
external/iris/iris/algebra/lib/gmap_view.v
external/iris/iris/algebra/lib/mono_nat.v
external/iris/iris/algebra/lib/gset_bij.v
external/iris/iris/si_logic/siprop.v
external/iris/iris/si_logic/bi.v
external/iris/iris/bi/notation.v
external/iris/iris/bi/interface.v
external/iris/iris/bi/derived_connectives.v
external/iris/iris/bi/extensions.v
external/iris/iris/bi/derived_laws.v
external/iris/iris/bi/derived_laws_later.v
external/iris/iris/bi/plainly.v
external/iris/iris/bi/internal_eq.v
external/iris/iris/bi/big_op.v
external/iris/iris/bi/updates.v
external/iris/iris/bi/ascii.v
external/iris/iris/bi/bi.v
external/iris/iris/bi/monpred.v
external/iris/iris/bi/embedding.v
external/iris/iris/bi/weakestpre.v
external/iris/iris/bi/telescopes.v
external/iris/iris/bi/lib/counterexamples.v
external/iris/iris/bi/lib/fixpoint.v
external/iris/iris/bi/lib/fractional.v
external/iris/iris/bi/lib/laterable.v
external/iris/iris/bi/lib/atomic.v
external/iris/iris/bi/lib/core.v
external/iris/iris/bi/lib/relations.v
external/iris/iris/base_logic/upred.v
external/iris/iris/base_logic/bi.v
external/iris/iris/base_logic/derived.v
external/iris/iris/base_logic/proofmode.v
external/iris/iris/base_logic/base_logic.v
external/iris/iris/base_logic/algebra.v
external/iris/iris/base_logic/bupd_alt.v
external/iris/iris/base_logic/lib/iprop.v
external/iris/iris/base_logic/lib/own.v
external/iris/iris/base_logic/lib/saved_prop.v
external/iris/iris/base_logic/lib/wsat.v
external/iris/iris/base_logic/lib/invariants.v
external/iris/iris/base_logic/lib/fancy_updates.v
external/iris/iris/base_logic/lib/boxes.v
external/iris/iris/base_logic/lib/na_invariants.v
external/iris/iris/base_logic/lib/cancelable_invariants.v
external/iris/iris/base_logic/lib/gen_heap.v
external/iris/iris/base_logic/lib/gen_inv_heap.v
external/iris/iris/base_logic/lib/fancy_updates_from_vs.v
external/iris/iris/base_logic/lib/proph_map.v
external/iris/iris/base_logic/lib/ghost_var.v
external/iris/iris/base_logic/lib/mono_nat.v
external/iris/iris/base_logic/lib/gset_bij.v
external/iris/iris/base_logic/lib/ghost_map.v
external/iris/iris/program_logic/adequacy.v
external/iris/iris/program_logic/lifting.v
external/iris/iris/program_logic/weakestpre.v
external/iris/iris/program_logic/total_weakestpre.v
external/iris/iris/program_logic/total_adequacy.v
external/iris/iris/program_logic/language.v
external/iris/iris/program_logic/ectx_language.v
external/iris/iris/program_logic/ectxi_language.v
external/iris/iris/program_logic/ectx_lifting.v
external/iris/iris/program_logic/ownp.v
external/iris/iris/program_logic/total_lifting.v
external/iris/iris/program_logic/total_ectx_lifting.v
external/iris/iris/program_logic/atomic.v
external/iris/iris/proofmode/base.v
external/iris/iris/proofmode/ident_name.v
external/iris/iris/proofmode/string_ident.v
external/iris/iris/proofmode/tokens.v
external/iris/iris/proofmode/coq_tactics.v
external/iris/iris/proofmode/ltac_tactics.v
external/iris/iris/proofmode/environments.v
external/iris/iris/proofmode/reduction.v
external/iris/iris/proofmode/intro_patterns.v
external/iris/iris/proofmode/spec_patterns.v
external/iris/iris/proofmode/sel_patterns.v
external/iris/iris/proofmode/tactics.v
external/iris/iris/proofmode/notation.v
external/iris/iris/proofmode/classes.v
external/iris/iris/proofmode/class_instances.v
external/iris/iris/proofmode/class_instances_later.v
external/iris/iris/proofmode/class_instances_updates.v
external/iris/iris/proofmode/class_instances_embedding.v
external/iris/iris/proofmode/class_instances_plainly.v
external/iris/iris/proofmode/class_instances_internal_eq.v
external/iris/iris/proofmode/frame_instances.v
external/iris/iris/proofmode/monpred.v
external/iris/iris/proofmode/modalities.v
external/iris/iris/proofmode/modality_instances.v
external/stdpp/theories/options.v
external/stdpp/theories/base.v
external/stdpp/theories/tactics.v
external/stdpp/theories/option.v
external/stdpp/theories/fin_map_dom.v
external/stdpp/theories/boolset.v
external/stdpp/theories/fin_maps.v
external/stdpp/theories/fin.v
external/stdpp/theories/vector.v
external/stdpp/theories/pmap.v
external/stdpp/theories/stringmap.v
external/stdpp/theories/fin_sets.v
external/stdpp/theories/mapset.v
external/stdpp/theories/proof_irrel.v
external/stdpp/theories/hashset.v
external/stdpp/theories/pretty.v
external/stdpp/theories/countable.v
external/stdpp/theories/orders.v
external/stdpp/theories/natmap.v
external/stdpp/theories/strings.v
external/stdpp/theories/relations.v
external/stdpp/theories/sets.v
external/stdpp/theories/listset.v
external/stdpp/theories/streams.v
external/stdpp/theories/gmap.v
external/stdpp/theories/gmultiset.v
external/stdpp/theories/prelude.v
external/stdpp/theories/listset_nodup.v
external/stdpp/theories/finite.v
external/stdpp/theories/numbers.v
external/stdpp/theories/nmap.v
external/stdpp/theories/zmap.v
external/stdpp/theories/coPset.v
external/stdpp/theories/coGset.v
external/stdpp/theories/lexico.v
external/stdpp/theories/propset.v
external/stdpp/theories/decidable.v
external/stdpp/theories/list.v
external/stdpp/theories/list_numbers.v
external/stdpp/theories/functions.v
external/stdpp/theories/hlist.v
external/stdpp/theories/sorting.v
external/stdpp/theories/infinite.v
external/stdpp/theories/nat_cancel.v
external/stdpp/theories/namespaces.v
external/stdpp/theories/telescopes.v
external/stdpp/theories/binders.v