-
Notifications
You must be signed in to change notification settings - Fork 6
/
_CoqProject.in
440 lines (440 loc) · 14.3 KB
/
_CoqProject.in
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
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
-R Bedrock Bedrock
-I Bedrock/reification
Bedrock/AMD64_gas.v
Bedrock/Allocated.v
Bedrock/Arrays.v
Bedrock/Bedrock.v
Bedrock/CancelIL.v
Bedrock/Decidables.v
Bedrock/DepList.v
Bedrock/Env.v
Bedrock/EqdepClass.v
Bedrock/Expr.v
Bedrock/ExprUnify.v
Bedrock/FastString.v
Bedrock/Folds.v
Bedrock/GenRec.v
Bedrock/Heaps.v
Bedrock/I386_gas.v
Bedrock/IL.v
Bedrock/ILEnv.v
Bedrock/ILTacCommon.v
Bedrock/ILTacLtac.v
Bedrock/ILTacML.v
Bedrock/LabelMap.v
Bedrock/Labels.v
Bedrock/Linker.v
Bedrock/ListFacts.v
Bedrock/Memory.v
Bedrock/Multimap.v
Bedrock/NatMap.v
Bedrock/Nomega.v
Bedrock/Ordering.v
Bedrock/Programming.v
Bedrock/PropX.v
Bedrock/PropXRel.v
Bedrock/PropXTac.v
Bedrock/Prover.v
Bedrock/Provers.v
Bedrock/Reflect.v
Bedrock/Reflection.v
Bedrock/ReifyExpr.v
Bedrock/ReifyHints.v
Bedrock/ReifyIL.v
Bedrock/ReifySepExpr.v
Bedrock/SepCancel.v
Bedrock/SepExpr.v
Bedrock/SepHeap.v
Bedrock/SepIL.v
Bedrock/SepLemma.v
Bedrock/SepTheoryX.v
Bedrock/SepTheoryXIL.v
Bedrock/SepUnify.v
Bedrock/StringSet.v
Bedrock/Structured.v
Bedrock/StructuredModule.v
Bedrock/SymEval.v
Bedrock/SymIL.v
Bedrock/SymILProofs.v
Bedrock/SymILTac.v
Bedrock/TacPackIL.v
Bedrock/Tactics.v
Bedrock/Thumb2_gas.v
Bedrock/TypedPackage.v
Bedrock/Unfolder.v
Bedrock/Word.v
Bedrock/XCAP.v
Bedrock/Examples/Arr.v
Bedrock/Examples/ArrayQuery.v
Bedrock/Examples/ArrayQueryTest.v
Bedrock/Examples/AutoSep.v
Bedrock/Examples/AutoSepExt.v
Bedrock/Examples/Baby.v
Bedrock/Examples/Bags.v
Bedrock/Examples/Conditional.v
Bedrock/Examples/ConditionalTest.v
Bedrock/Examples/Factorial.v
Bedrock/Examples/Indir.v
Bedrock/Examples/Lambda.v
Bedrock/Examples/LambdaTest.v
Bedrock/Examples/LemmaTests.v
Bedrock/Examples/ListSet.v
Bedrock/Examples/Malloc.v
Bedrock/Examples/Memoize.v
Bedrock/Examples/Pair.v
Bedrock/Examples/PreAutoSep.v
Bedrock/Examples/Queue.v
Bedrock/Examples/Sets.v
Bedrock/Examples/SinglyLinkedList.v
Bedrock/Examples/StreamParse.v
Bedrock/Examples/StreamParseTest.v
Bedrock/Examples/Swap.v
Bedrock/Examples/TreeSet.v
Bedrock/Examples/TrivialArray.v
Bedrock/Examples/TrivialMem.v
Bedrock/Examples/TrivialMem2.v
Bedrock/Examples/Wrap.v
Bedrock/Examples/comparison/Combined.v
Bedrock/Examples/comparison/Server.v
Bedrock/Examples/x86/FactorialAMD64.v
Bedrock/Platform/ArrayOps.v
Bedrock/Platform/Arrays8.v
Bedrock/Platform/AutoSep.v
Bedrock/Platform/AutoSepExt.v
Bedrock/Platform/Bags.v
Bedrock/Platform/Bootstrap.v
Bedrock/Platform/Buffers.v
Bedrock/Platform/Conditional.v
Bedrock/Platform/Http.v
Bedrock/Platform/HttpQ.v
Bedrock/Platform/Io.v
Bedrock/Platform/ListSegment.v
Bedrock/Platform/Malloc.v
Bedrock/Platform/Misc.v
Bedrock/Platform/MoreArrays.v
Bedrock/Platform/NumOps.v
Bedrock/Platform/PreAutoSep.v
Bedrock/Platform/Queue.v
Bedrock/Platform/RelDb.v
Bedrock/Platform/RelDbCondition.v
Bedrock/Platform/RelDbDelete.v
Bedrock/Platform/RelDbInsert.v
Bedrock/Platform/RelDbSelect.v
Bedrock/Platform/Safety.v
Bedrock/Platform/Scheduler.v
Bedrock/Platform/Sets.v
Bedrock/Platform/SinglyLinkedList.v
Bedrock/Platform/StringOps.v
Bedrock/Platform/Sys.v
Bedrock/Platform/Thread.v
Bedrock/Platform/ThreadQueue.v
Bedrock/Platform/ThreadQueues.v
Bedrock/Platform/Util.v
Bedrock/Platform/Wrap.v
Bedrock/Platform/Xml.v
Bedrock/Platform/XmlLang.v
Bedrock/Platform/XmlLex.v
Bedrock/Platform/XmlOutput.v
Bedrock/Platform/XmlProg.v
Bedrock/Platform/XmlSearch.v
Bedrock/Platform/Cito/ADT.v
Bedrock/Platform/Cito/AxSpec.v
Bedrock/Platform/Cito/BedrockTactics.v
Bedrock/Platform/Cito/BoolFacts.v
Bedrock/Platform/Cito/CModule.v
Bedrock/Platform/Cito/CModuleFacts.v
Bedrock/Platform/Cito/ChangeSpec.v
Bedrock/Platform/Cito/CompileExpr.v
Bedrock/Platform/Cito/CompileExprs.v
Bedrock/Platform/Cito/CompileFunc.v
Bedrock/Platform/Cito/CompileFuncImpl.v
Bedrock/Platform/Cito/CompileFuncSpec.v
Bedrock/Platform/Cito/CompileModule.v
Bedrock/Platform/Cito/CompileModule2.v
Bedrock/Platform/Cito/CompileStmt.v
Bedrock/Platform/Cito/CompileStmtImpl.v
Bedrock/Platform/Cito/CompileStmtSpec.v
Bedrock/Platform/Cito/CompileStmtTactics.v
Bedrock/Platform/Cito/ConvertLabel.v
Bedrock/Platform/Cito/ConvertLabelMap.v
Bedrock/Platform/Cito/Depth.v
Bedrock/Platform/Cito/DepthExpr.v
Bedrock/Platform/Cito/Dict.v
Bedrock/Platform/Cito/ExprLemmas.v
Bedrock/Platform/Cito/F.v
Bedrock/Platform/Cito/FMapFacts1.v
Bedrock/Platform/Cito/FMapFacts2.v
Bedrock/Platform/Cito/FSetFacts1.v
Bedrock/Platform/Cito/FreeVars.v
Bedrock/Platform/Cito/FreeVarsExpr.v
Bedrock/Platform/Cito/FuncCore.v
Bedrock/Platform/Cito/GLabel.v
Bedrock/Platform/Cito/GLabelKey.v
Bedrock/Platform/Cito/GLabelMap.v
Bedrock/Platform/Cito/GLabelMapFacts.v
Bedrock/Platform/Cito/GeneralTactics.v
Bedrock/Platform/Cito/GeneralTactics2.v
Bedrock/Platform/Cito/GeneralTactics3.v
Bedrock/Platform/Cito/GeneralTactics4.v
Bedrock/Platform/Cito/GeneralTactics5.v
Bedrock/Platform/Cito/GetLocalVars.v
Bedrock/Platform/Cito/GetLocalVarsFacts.v
Bedrock/Platform/Cito/GoodFunc.v
Bedrock/Platform/Cito/GoodFunction.v
Bedrock/Platform/Cito/GoodModule.v
Bedrock/Platform/Cito/GoodModuleDec.v
Bedrock/Platform/Cito/GoodModuleDecFacts.v
Bedrock/Platform/Cito/GoodOptimizer.v
Bedrock/Platform/Cito/IffFacts.v
Bedrock/Platform/Cito/Inv.v
Bedrock/Platform/Cito/InvFacts.v
Bedrock/Platform/Cito/IsGoodModule.v
Bedrock/Platform/Cito/Label2Word.v
Bedrock/Platform/Cito/Label2WordFacts.v
Bedrock/Platform/Cito/LabelMapFacts.v
Bedrock/Platform/Cito/LayoutHints.v
Bedrock/Platform/Cito/LayoutHints2.v
Bedrock/Platform/Cito/LayoutHints3.v
Bedrock/Platform/Cito/LayoutHints4.v
Bedrock/Platform/Cito/LayoutHintsUtil.v
Bedrock/Platform/Cito/Link.v
Bedrock/Platform/Cito/LinkFacts.v
Bedrock/Platform/Cito/LinkModuleImpls.v
Bedrock/Platform/Cito/LinkSpec.v
Bedrock/Platform/Cito/LinkSpecFacts.v
Bedrock/Platform/Cito/ListFacts1.v
Bedrock/Platform/Cito/ListFacts2.v
Bedrock/Platform/Cito/ListFacts3.v
Bedrock/Platform/Cito/ListFacts4.v
Bedrock/Platform/Cito/ListFacts5.v
Bedrock/Platform/Cito/ListNotationsFix.v
Bedrock/Platform/Cito/MakeADT.v
Bedrock/Platform/Cito/MakeWrapper.v
Bedrock/Platform/Cito/Max.v
Bedrock/Platform/Cito/MaxFacts.v
Bedrock/Platform/Cito/MyFree.v
Bedrock/Platform/Cito/MyMalloc.v
Bedrock/Platform/Cito/NameDecoration.v
Bedrock/Platform/Cito/NameVC.v
Bedrock/Platform/Cito/NatFacts.v
Bedrock/Platform/Cito/NoUninitDec.v
Bedrock/Platform/Cito/NoUninitDecFacts.v
Bedrock/Platform/Cito/Notations3.v
Bedrock/Platform/Cito/Notations4.v
Bedrock/Platform/Cito/NotationsExpr.v
Bedrock/Platform/Cito/Option.v
Bedrock/Platform/Cito/PostOk.v
Bedrock/Platform/Cito/ProgramLogic.v
Bedrock/Platform/Cito/ProgramLogic2.v
Bedrock/Platform/Cito/RepInv.v
Bedrock/Platform/Cito/S.v
Bedrock/Platform/Cito/SaveRet.v
Bedrock/Platform/Cito/Semantics.v
Bedrock/Platform/Cito/SemanticsExpr.v
Bedrock/Platform/Cito/SemanticsExprLemmas.v
Bedrock/Platform/Cito/SemanticsFacts.v
Bedrock/Platform/Cito/SemanticsFacts2.v
Bedrock/Platform/Cito/SemanticsFacts3.v
Bedrock/Platform/Cito/SemanticsFacts4.v
Bedrock/Platform/Cito/SemanticsFacts5.v
Bedrock/Platform/Cito/SemanticsFacts6.v
Bedrock/Platform/Cito/SemanticsFacts7.v
Bedrock/Platform/Cito/SemanticsFacts8.v
Bedrock/Platform/Cito/SemanticsFacts9.v
Bedrock/Platform/Cito/SemanticsUtil.v
Bedrock/Platform/Cito/SepHints.v
Bedrock/Platform/Cito/SepHints2.v
Bedrock/Platform/Cito/SepHints3.v
Bedrock/Platform/Cito/SepHints4.v
Bedrock/Platform/Cito/SepHints5.v
Bedrock/Platform/Cito/SepHintsUtil.v
Bedrock/Platform/Cito/SepLemmas.v
Bedrock/Platform/Cito/SetoidListFacts.v
Bedrock/Platform/Cito/StringFacts2.v
Bedrock/Platform/Cito/StringMap.v
Bedrock/Platform/Cito/StringMapFacts.v
Bedrock/Platform/Cito/StringSetFacts.v
Bedrock/Platform/Cito/StringSetTactics.v
Bedrock/Platform/Cito/StructuredModuleFacts.v
Bedrock/Platform/Cito/Stub.v
Bedrock/Platform/Cito/Stubs.v
Bedrock/Platform/Cito/SynReqFacts.v
Bedrock/Platform/Cito/SynReqFacts2.v
Bedrock/Platform/Cito/SynReqFacts3.v
Bedrock/Platform/Cito/SynReqFactsUtil.v
Bedrock/Platform/Cito/Syntax.v
Bedrock/Platform/Cito/SyntaxExpr.v
Bedrock/Platform/Cito/SyntaxFunc.v
Bedrock/Platform/Cito/SyntaxModule.v
Bedrock/Platform/Cito/SyntaxNotations.v
Bedrock/Platform/Cito/Transit.v
Bedrock/Platform/Cito/TryModule.v
Bedrock/Platform/Cito/Union.v
Bedrock/Platform/Cito/ValsStringSet.v
Bedrock/Platform/Cito/VerifCondOk.v
Bedrock/Platform/Cito/VerifCondOkCall.v
Bedrock/Platform/Cito/VerifCondOkNonCall.v
Bedrock/Platform/Cito/VerifCondOkNonCall2.v
Bedrock/Platform/Cito/VerifCondOkTactics.v
Bedrock/Platform/Cito/WellFormed.v
Bedrock/Platform/Cito/Wf.v
Bedrock/Platform/Cito/WordFacts.v
Bedrock/Platform/Cito/WordFacts2.v
Bedrock/Platform/Cito/WordFacts3.v
Bedrock/Platform/Cito/WordFacts4.v
Bedrock/Platform/Cito/WordFacts5.v
Bedrock/Platform/Cito/WordFacts6.v
Bedrock/Platform/Cito/WordKey.v
Bedrock/Platform/Cito/WordMap.v
Bedrock/Platform/Cito/WordMapFacts.v
Bedrock/Platform/Cito/adt/TabledADT.v
Bedrock/Platform/Cito/examples/ArraySeq.v
Bedrock/Platform/Cito/examples/Cell.v
Bedrock/Platform/Cito/examples/CountUnique.v
Bedrock/Platform/Cito/examples/CountUniqueAMD64.v
Bedrock/Platform/Cito/examples/CountUniqueDriver.v
Bedrock/Platform/Cito/examples/ExampleADT.v
Bedrock/Platform/Cito/examples/ExampleImpl.v
Bedrock/Platform/Cito/examples/ExampleRepInv.v
Bedrock/Platform/Cito/examples/Factorial.v
Bedrock/Platform/Cito/examples/FactorialAMD64.v
Bedrock/Platform/Cito/examples/FactorialDriver.v
Bedrock/Platform/Cito/examples/FactorialRecur.v
Bedrock/Platform/Cito/examples/FactorialRecurAMD64.v
Bedrock/Platform/Cito/examples/FactorialRecurDriver.v
Bedrock/Platform/Cito/examples/FiniteSet.v
Bedrock/Platform/Cito/examples/ListSet.v
Bedrock/Platform/Cito/examples/ReturnZero.v
Bedrock/Platform/Cito/examples/ReturnZeroAMD64.v
Bedrock/Platform/Cito/examples/ReturnZeroDriver.v
Bedrock/Platform/Cito/examples/Seq.v
Bedrock/Platform/Cito/examples/SimpleCell.v
Bedrock/Platform/Cito/examples/UseCell.v
Bedrock/Platform/Cito/examples/UseCellAMD64.v
Bedrock/Platform/Cito/examples/UseCellDriver.v
Bedrock/Platform/Cito/optimizers/ConstFolding.v
Bedrock/Platform/Cito/optimizers/ElimDead.v
Bedrock/Platform/Cito/optimizers/Identity.v
Bedrock/Platform/Facade/Compile.v
Bedrock/Platform/Facade/CompileDFModule.v
Bedrock/Platform/Facade/CompileDFacade.v
Bedrock/Platform/Facade/CompileDFacadeCorrect.v
Bedrock/Platform/Facade/CompileDFacadeToCito.v
Bedrock/Platform/Facade/CompileModule.v
Bedrock/Platform/Facade/CompileOut.v
Bedrock/Platform/Facade/CompileOut2.v
Bedrock/Platform/Facade/CompileRunsTo.v
Bedrock/Platform/Facade/CompileSafe.v
Bedrock/Platform/Facade/CompileUnit.v
Bedrock/Platform/Facade/CompileUnit2.v
Bedrock/Platform/Facade/DFModule.v
Bedrock/Platform/Facade/DFacade.v
Bedrock/Platform/Facade/DFacadeFacts.v
Bedrock/Platform/Facade/DFacadeFacts2.v
Bedrock/Platform/Facade/DFacadeToBedrock.v
Bedrock/Platform/Facade/DFacadeToBedrock2.v
Bedrock/Platform/Facade/DFacadeToBedrock2Util.v
Bedrock/Platform/Facade/FModule.v
Bedrock/Platform/Facade/Facade.v
Bedrock/Platform/Facade/FacadeFacts.v
Bedrock/Platform/Facade/Listy.v
Bedrock/Platform/Facade/NameDecoration.v
Bedrock/Platform/Facade/Notations.v
Bedrock/Platform/Facade/SafeCoind.v
Bedrock/Platform/Facade/examples/ArrayTupleF.v
Bedrock/Platform/Facade/examples/ExtractCompiler.v
Bedrock/Platform/Facade/examples/FiatADTs.v
Bedrock/Platform/Facade/examples/FiatImpl.v
Bedrock/Platform/Facade/examples/FiatRepInv.v
Bedrock/Platform/Facade/examples/FiniteSetF.v
Bedrock/Platform/Facade/examples/ListSeqF.v
Bedrock/Platform/Facade/examples/ListSetF.v
Bedrock/Platform/Facade/examples/NotationExample.v
Bedrock/Platform/Facade/examples/QsADTs.v
Bedrock/Platform/Facade/examples/QsImpl.v
Bedrock/Platform/Facade/examples/QsRepInv.v
Bedrock/Platform/Facade/examples/SeqF.v
Bedrock/Platform/Facade/examples/TestLinking.v
Bedrock/Platform/Facade/examples/TestLinking2.v
Bedrock/Platform/Facade/examples/TupleF.v
Bedrock/Platform/Facade/examples/TupleListF.v
Bedrock/Platform/Facade/examples/TupleSeqF.v
Bedrock/Platform/Facade/examples/Tuples0F.v
Bedrock/Platform/Facade/examples/Tuples1F.v
Bedrock/Platform/Facade/examples/Tuples2F.v
Bedrock/Platform/Facade/examples/TuplesF.v
Bedrock/Platform/tests/Abort.v
Bedrock/Platform/tests/AbortAMD64.v
Bedrock/Platform/tests/AbortDriver.v
Bedrock/Platform/tests/ArrayTest.v
Bedrock/Platform/tests/ArrayTestAMD64.v
Bedrock/Platform/tests/ArrayTestDriver.v
Bedrock/Platform/tests/BabyThread.v
Bedrock/Platform/tests/BabyThreadDriver.v
Bedrock/Platform/tests/CallbackAMD64.v
Bedrock/Platform/tests/CallbackDriver.v
Bedrock/Platform/tests/Connect.v
Bedrock/Platform/tests/ConnectAMD64.v
Bedrock/Platform/tests/ConnectDriver.v
Bedrock/Platform/tests/Echo.v
Bedrock/Platform/tests/Echo2.v
Bedrock/Platform/tests/Echo2AMD64.v
Bedrock/Platform/tests/Echo2Driver.v
Bedrock/Platform/tests/Echo3.v
Bedrock/Platform/tests/Echo3AMD64.v
Bedrock/Platform/tests/Echo3Driver.v
Bedrock/Platform/tests/EchoAMD64.v
Bedrock/Platform/tests/EchoDriver.v
Bedrock/Platform/tests/EchoServer.v
Bedrock/Platform/tests/EchoServerAMD64.v
Bedrock/Platform/tests/EchoServerDriver.v
Bedrock/Platform/tests/Increment.v
Bedrock/Platform/tests/LinkTest.v
Bedrock/Platform/tests/ListBuilder.v
Bedrock/Platform/tests/ListBuilderAMD64.v
Bedrock/Platform/tests/ListBuilderDriver.v
Bedrock/Platform/tests/MiniMasterAMD64.v
Bedrock/Platform/tests/MiniMasterDriver.v
Bedrock/Platform/tests/MiniMasterI386.v
Bedrock/Platform/tests/PrintInt.v
Bedrock/Platform/tests/PrintIntAMD64.v
Bedrock/Platform/tests/PrintIntDriver.v
Bedrock/Platform/tests/Ros.v
Bedrock/Platform/tests/RosMasterAMD64.v
Bedrock/Platform/tests/RosMasterDriver.v
Bedrock/Platform/tests/RosMasterI386.v
Bedrock/Platform/tests/RtosAMD64.v
Bedrock/Platform/tests/RtosDriver.v
Bedrock/Platform/tests/RtosI386.v
Bedrock/Platform/tests/SharedList.v
Bedrock/Platform/tests/SharedListAMD64.v
Bedrock/Platform/tests/SharedListDriver.v
Bedrock/Platform/tests/Spawn.v
Bedrock/Platform/tests/StringDb.v
Bedrock/Platform/tests/Thread0.v
Bedrock/Platform/tests/WebServer.v
Bedrock/Platform/tests/WebServerAMD64.v
Bedrock/Platform/tests/WebServerDriver.v
Bedrock/Platform/tests/XmlTest2AMD64.v
Bedrock/Platform/tests/XmlTest2Driver.v
Bedrock/Platform/tests/XmlTestAMD64.v
Bedrock/Platform/tests/XmlTestDriver.v
Bedrock/Platform/tests/Yield.v
Bedrock/provers/ArrayBoundProver.v
Bedrock/provers/AssumptionProver.v
Bedrock/provers/LocalsProver.v
Bedrock/provers/ReflexivityProver.v
Bedrock/provers/TransitivityProver.v
Bedrock/provers/WordProver.v
Bedrock/reification/example.v
Bedrock/sep/Array.v
Bedrock/sep/Array8.v
Bedrock/sep/Locals.v
Bedrock/sep/PtsTo.v
Bedrock/ILTac.v
Bedrock/Coq__8_4__8_5__Compat.v
Bedrock/reification/extlib.ml
Bedrock/reification/extlib.mli
Bedrock/reification/reif.ml4
Bedrock/reification/reif.mllib
Bedrock/reification/reif_tactics.ml