-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy path_CoqProject
93 lines (84 loc) · 3.11 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
-Q theories VLSM
-arg -w -arg -future-coercion-class-field
-arg -w -arg -deprecated-tacopt-without-locality
theories/Lib/Itauto.v
theories/Lib/Ctauto.v
theories/Lib/SsrExport.v
theories/Lib/Preamble.v
theories/Lib/EquationsExtras.v
theories/Lib/FinSuppFn.v
theories/Lib/NatExtras.v
theories/Lib/ListExtras.v
theories/Lib/StdppExtras.v
theories/Lib/StdppListSet.v
theories/Lib/ListSetExtras.v
theories/Lib/SortedLists.v
theories/Lib/FinSetExtras.v
theories/Lib/RealsExtras.v
theories/Lib/TopSort.v
theories/Lib/NeList.v
theories/Lib/StreamExtras.v
theories/Lib/StreamFilters.v
theories/Lib/Traces.v
theories/Lib/TraceProperties.v
theories/Lib/TraceClassicalProperties.v
theories/Lib/Measurable.v
theories/Core/VLSM.v
theories/Core/PreloadedVLSM.v
theories/Core/Plans.v
theories/Core/VLSMProjections/VLSMPartialProjection.v
theories/Core/VLSMProjections/VLSMStutteringEmbedding.v
theories/Core/VLSMProjections/VLSMTotalProjection.v
theories/Core/VLSMProjections/VLSMEmbedding.v
theories/Core/VLSMProjections/VLSMInclusion.v
theories/Core/VLSMProjections/VLSMEquality.v
theories/Core/VLSMProjections.v
theories/Core/ConstrainedVLSM.v
theories/Core/Composition.v
theories/Core/Validator.v
theories/Core/ProjectionTraces.v
theories/Core/ReachableThreshold.v
theories/Core/Equivocation.v
theories/Core/EquivocationProjections.v
theories/Core/Equivocation/NoEquivocation.v
theories/Core/SubProjectionTraces.v
theories/Core/MessageDependencies.v
theories/Core/AnnotatedVLSM.v
theories/Core/ByzantineTraces.v
theories/Core/TraceableVLSM.v
theories/Core/HistoryVLSM.v
theories/Core/Validators/FreeCompositionValidator.v
theories/Core/Equivocation/FixedSetEquivocation.v
theories/Core/Equivocation/MsgDepFixedSetEquivocation.v
theories/Core/Equivocation/TraceWiseEquivocation.v
theories/Core/Equivocation/WitnessedEquivocation.v
theories/Core/Equivocation/FullNode.v
theories/Core/Equivocation/LimitedMessageEquivocation.v
theories/Core/Equivocation/MsgDepLimitedEquivocation.v
theories/Core/Equivocation/MinimalEquivocationTrace.v
theories/Core/Equivocators/Equivocators.v
theories/Core/Equivocators/EquivocatorsProjections.v
theories/Core/Equivocators/MessageProperties.v
theories/Core/Equivocators/EquivocatorReplay.v
theories/Core/Equivocators/EquivocatorsComposition.v
theories/Core/Equivocators/EquivocatorsCompositionProjections.v
theories/Core/Equivocators/FullReplayTraces.v
theories/Core/Equivocators/SimulatingFree.v
theories/Core/Equivocators/FixedEquivocation.v
theories/Core/Equivocators/FixedEquivocationSimulation.v
theories/Core/Equivocators/LimitedStateEquivocation.v
theories/Core/Equivocators/LimitedEquivocationSimulation.v
theories/Core/ByzantineTraces/FixedSetByzantineTraces.v
theories/Core/ByzantineTraces/LimitedByzantineTraces.v
theories/Examples/Tutorial/Multiply.v
theories/Examples/Tutorial/PrimesComposition.v
theories/Examples/Tutorial/Formulas.v
theories/Examples/Tutorial/MuddyChildrenRounds.v
theories/Examples/ELMO/BaseELMO.v
theories/Examples/ELMO/UMO.v
theories/Examples/ELMO/MO.v
theories/Examples/ELMO/ELMO.v
theories/Examples/ELMO/AllELMO.v
theories/Examples/Paxos/Consensus.v
theories/Examples/Paxos/Voting.v
theories/Examples/Paxos/Paxos.v