forked from shentufoundation/deepsea
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy path_CoqProject
74 lines (71 loc) · 1.51 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
-R . DeepSpec
-arg -w
-arg none
cclib/Integers.v
cclib/Coqlib.v
backend/AST.v
cclib/Maps.v
cclib/Errors.v
lib/Monad/Functor.v
lib/Monad/Applicative.v
lib/Monad/MonadZero.v
lib/Monad/MonadPlus.v
lib/Monad/MonadTrans.v
lib/Monad/MonadReader.v
lib/Monad/MonadExc.v
lib/Monad/OptErrMonadLaws.v
lib/Monad/OptErrMonad.v
lib/Monad/OptionMonadLaws.v
lib/Monad/MonadState.v
lib/Monad/MonadLaws.v
lib/Monad/MonadInv.v
lib/Monad/OptionMonad.v
lib/Monad/RunStateTInv.v
backend/Smallstep.v
backend/Events.v
backend/phase/MiniC/BigstepSemantics.v
backend/Environments/HashEnv.v
backend/Environments/StackEnv.v
backend/MachineModelLow.v
backend/Expressions/ExpStacked.v
backend/GasModel.v
backend/phase/MiniC/Semantics.v
backend/TempModel.v
backend/Expressions/SemanticsMiniC.v
core/SynthesisExpr.v
core/SynthesisStmt.v
lib/LangDef.v
lib/IndexedMaps.v
core/SynthesisFunc.v
lib/Monad/StateMonadLaws.v
lib/Monad/StateMonad.v
lib/Monad/StateMonadOption.v
backend/Environments/Globalenvs.v
backend/Expressions/ExpMiniC.v
backend/Statements/StmtMiniC.v
core/Syntax.v
core/HyperTypeInst.v
lib/SimpleIndexedMaps.v
lib/SimpleMaps.v
lib/Monad/ContOptionMonad.v
lib/OProp.v
lib/Lens.v
core/MemoryModel.v
backend/AbstractData.v
backend/MachineModel.v
core/HyperType.v
backend/MemoryModel.v
backend/Environments/AllEnvironments.v
core/SEnv.v
lib/ArithInv.v
backend/Environments/ExtEnv.v
core/Cval.v
backend/SymbolicKeccak.v
lib/Monad/Monad.v
backend/Options.v
backend/Ctypes.v
backend/Values/HighValues.v
backend/IndexLib.v
backend/Values/LowValues.v
backend/Cop.v
Runtime.v