1 | utilities/extralib.ma: redundant basics/lists/list.ma |
---|
2 | utilities/extralib.ma: redundant basics/types.ma |
---|
3 | utilities/monad.ma: redundant basics/relations.ma |
---|
4 | utilities/monad.ma: redundant basics/types.ma |
---|
5 | utilities/option.ma: redundant basics/types.ma |
---|
6 | utilities/extranat.ma: redundant basics/types.ma |
---|
7 | ASM/Vector.ma: redundant arithmetics/nat.ma |
---|
8 | ASM/Vector.ma: redundant basics/types.ma |
---|
9 | ASM/Vector.ma: redundant basics/lists/list.ma |
---|
10 | ASM/BitVector.ma: redundant arithmetics/nat.ma |
---|
11 | common/PositiveMap.ma: redundant basics/types.ma |
---|
12 | common/Errors.ma: redundant utilities/monad.ma |
---|
13 | common/Errors.ma: redundant basics/russell.ma |
---|
14 | common/Errors.ma: redundant basics/lists/list.ma |
---|
15 | common/Errors.ma: redundant basics/logic.ma |
---|
16 | common/Errors.ma: redundant basics/types.ma |
---|
17 | utilities/lists.ma: redundant utilities/monad.ma |
---|
18 | utilities/lists.ma: redundant utilities/option.ma |
---|
19 | utilities/lists.ma: redundant basics/lists/list.ma |
---|
20 | common/Identifiers.ma: redundant utilities/binary/positive.ma |
---|
21 | common/Identifiers.ma: redundant basics/types.ma |
---|
22 | common/Integers.ma: redundant ASM/BitVector.ma |
---|
23 | common/Integers.ma: redundant utilities/extranat.ma |
---|
24 | common/Integers.ma: redundant arithmetics/nat.ma |
---|
25 | common/AST.ma: redundant basics/types.ma |
---|
26 | ASM/BitVectorZ.ma: redundant ASM/BitVector.ma |
---|
27 | ASM/BitVectorZ.ma: redundant utilities/binary/Z.ma |
---|
28 | common/Values.ma: redundant common/Errors.ma |
---|
29 | utilities/Coqlib.ma: redundant basics/lists/list.ma |
---|
30 | utilities/Coqlib.ma: redundant basics/types.ma |
---|
31 | common/GenMem.ma: redundant common/Pointers.ma |
---|
32 | common/GenMem.ma: redundant utilities/extralib.ma |
---|
33 | common/Globalenvs.ma: redundant common/AST.ma |
---|
34 | common/Globalenvs.ma: redundant common/Errors.ma |
---|
35 | common/extraGlobalenvs.ma: redundant common/AST.ma |
---|
36 | common/ExtraMonads.ma: redundant common/Errors.ma |
---|
37 | utilities/bind_new.ma: redundant utilities/monad.ma |
---|
38 | common/LabelledObjects.ma: redundant utilities/lists.ma |
---|
39 | joint/Joint.ma: redundant utilities/lists.ma |
---|
40 | common/Graphs.ma: redundant common/Identifiers.ma |
---|
41 | ASM/BitVectorTrie.ma: redundant basics/types.ma |
---|
42 | common/Graphs.ma: redundant basics/types.ma |
---|
43 | ASM/I8051.ma: redundant arithmetics/nat.ma |
---|
44 | joint/TranslateUtils.ma: redundant joint/Joint.ma |
---|
45 | joint/semanticsUtils.ma: redundant ASM/BitVectorTrie.ma |
---|
46 | joint/semanticsUtils.ma: redundant utilities/hide.ma |
---|
47 | joint/BEMem.ma: redundant common/ByteValues.ma |
---|
48 | common/Events.ma: redundant utilities/extralib.ma |
---|
49 | common/Events.ma: redundant basics/lists/list.ma |
---|
50 | joint/joint_semantics.ma: redundant common/Globalenvs.ma |
---|
51 | common/StructuredTraces.ma: redundant utilities/option.ma |
---|
52 | common/StructuredTraces.ma: redundant common/CostLabel.ma |
---|
53 | common/StructuredTraces.ma: redundant basics/bool.ma |
---|
54 | joint/semantics_blocks.ma: redundant joint/blocks.ma |
---|
55 | common/Animation.ma: redundant arithmetics/nat.ma |
---|
56 | common/SmallstepExec.ma: redundant common/Integers.ma |
---|
57 | common/SmallstepExec.ma: redundant utilities/extralib.ma |
---|
58 | Clight/Csyntax.ma: redundant common/Errors.ma |
---|
59 | Clight/Csem.ma: redundant Clight/Csyntax.ma |
---|
60 | Clight/Cexec.ma: redundant utilities/extralib.ma |
---|
61 | ERTLptr/ERTLptr_semantics.ma: redundant joint/semanticsUtils.ma |
---|
62 | Clight/frontend_misc.ma: redundant common/IOMonad.ma |
---|
63 | Clight/frontend_misc.ma: redundant common/Pointers.ma |
---|
64 | Clight/frontend_misc.ma: redundant Clight/TypeComparison.ma |
---|
65 | Clight/MemProperties.ma: redundant common/FrontEndMem.ma |
---|
66 | Clight/switchRemoval.ma: redundant utilities/extralib.ma |
---|
67 | Clight/switchRemoval.ma: redundant common/Identifiers.ma |
---|
68 | Clight/switchRemoval.ma: redundant basics/lists/listb.ma |
---|
69 | RTLabs/RTLabs_syntax.ma: redundant ASM/Vector.ma |
---|
70 | common/FrontEndOps.ma: redundant common/Values.ma |
---|
71 | RTLabs/RTLabs_syntax.ma: redundant common/AST.ma |
---|
72 | RTLabs/RTLabs_syntax.ma: redundant basics/logic.ma |
---|
73 | RTLabs/CostCheck.ma: redundant RTLabs/CostSpec.ma |
---|
74 | RTLabs/RTLabs_semantics.ma: redundant common/Errors.ma |
---|
75 | RTLabs/RTLabs_semantics.ma: redundant basics/lists/list.ma |
---|
76 | Cminor/toRTLabs.ma: redundant Cminor/Cminor_syntax.ma |
---|
77 | Cminor/toRTLabs.ma: redundant common/Globalenvs.ma |
---|
78 | Cminor/toRTLabs.ma: redundant utilities/lists.ma |
---|
79 | Cminor/Cminor_semantics.ma: redundant common/FrontEndMem.ma |
---|
80 | Cminor/Cminor_semantics.ma: redundant common/Events.ma |
---|
81 | Clight/toCminor.ma: redundant basics/lists/list.ma |
---|
82 | Clight/SimplifyCasts.ma: redundant Clight/Cexec.ma |
---|
83 | Clight/SimplifyCasts.ma: redundant Clight/TypeComparison.ma |
---|
84 | Clight/SimplifyCasts.ma: redundant Clight/Csyntax.ma |
---|
85 | ASM/UtilBranch.ma: redundant ASM/Util.ma |
---|
86 | ERTL/ERTLToERTLptr.ma: redundant ERTL/ERTL.ma |
---|
87 | RTLabs/RTLabs_traces.ma: redundant RTLabs/CostSpec.ma |
---|
88 | joint/extra_joint_semantics.ma: redundant joint/joint_semantics.ma |
---|
89 | ERTL/ERTLtoERTLptrUtils.ma: redundant common/ExtraMonads.ma |
---|
90 | ERTL/ERTLtoERTLptrUtils.ma: redundant joint/Traces.ma |
---|
91 | joint/StatusSimulationHelper.ma: redundant joint/Traces.ma |
---|
92 | joint/StatusSimulationHelper.ma: redundant joint/semanticsUtils.ma |
---|
93 | common/stacksize.ma: redundant basics/lists/list.ma |
---|
94 | ASM/Fetch.ma: redundant ASM/Arithmetic.ma |
---|
95 | ASM/Assembly.ma: redundant ASM/Arithmetic.ma |
---|
96 | ASM/Assembly.ma: redundant ASM/ASM.ma |
---|
97 | semantics.ma: redundant ERTL/ERTL_semantics.ma |
---|
98 | compiler.ma: redundant ASM/ASMCosts.ma |
---|
99 | ASM/PolicyFront.ma: redundant utilities/extralib.ma |
---|
100 | ASM/PolicyFront.ma: redundant ASM/Status.ma |
---|
101 | ASM/PolicyFront.ma: redundant ASM/Fetch.ma |
---|
102 | ASM/PolicyFront.ma: redundant ASM/Arithmetic.ma |
---|
103 | ASM/PolicyFront.ma: redundant ASM/ASM.ma |
---|
104 | LIN/LINToASM.ma: redundant ASM/Util.ma |
---|
105 | ERTLptr/ERTLptrToLTL.ma: redundant ASM/Arithmetic.ma |
---|
106 | utilities/adt/set_adt.ma: redundant arithmetics/nat.ma |
---|
107 | utilities/adt/set_adt.ma: redundant basics/lists/list.ma |
---|
108 | utilities/adt/set_adt.ma: redundant basics/types.ma |
---|
109 | ERTLptr/liveness.ma: redundant ASM/Util.ma |
---|
110 | RTL/RTLToERTL.ma: redundant common/Identifiers.ma |
---|
111 | RTLabs/RTLabsToRTL.ma: redundant common/Graphs.ma |
---|
112 | Clight/test/search.test.ma: redundant common/Animation.ma |
---|
113 | Clight/toCminorOps.ma: redundant Clight/frontend_misc.ma |
---|
114 | Clight/toCminorOps.ma: redundant Clight/Cexec.ma |
---|
115 | Clight/toCminorCorrectnessExpr.ma: redundant common/Globalenvs.ma |
---|
116 | Clight/toCminorCorrectnessExpr.ma: redundant Clight/toCminor.ma |
---|
117 | Clight/toCminorCorrectness.ma: redundant Cminor/Cminor_abstract.ma |
---|
118 | Clight/toCminorCorrectness.ma: redundant Clight/Clight_abstract.ma |
---|
119 | Clight/toCminorCorrectness.ma: redundant Clight/memoryInjections.ma |
---|
120 | Clight/toCminorCorrectness.ma: redundant common/Globalenvs.ma |
---|
121 | Clight/toCminorCorrectness.ma: redundant Clight/CexecInd.ma |
---|
122 | Clight/toCminorCorrectness.ma: redundant Clight/toCminor.ma |
---|
123 | utilities/adt/priority_set_adt.ma: redundant arithmetics/nat.ma |
---|
124 | utilities/adt/priority_set_adt.ma: redundant basics/lists/list.ma |
---|
125 | utilities/adt/priority_set_adt.ma: redundant basics/types.ma |
---|
126 | ASM/Test.ma: redundant ASM/StatusProofs.ma |
---|
127 | ASM/Test.ma: redundant ASM/Interpret.ma |
---|
128 | ASM/Test.ma: redundant ASM/Assembly.ma |
---|
129 | ERTLptr/ERTLptrToLTLProof.ma: redundant common/StatusSimulation.ma |
---|
130 | ERTLptr/ERTLptrToLTLProof.ma: redundant joint/Traces.ma |
---|
131 | Clight/test/castremoval.test.ma: redundant common/Animation.ma |
---|
132 | ASM/WellLabeled.ma: redundant ASM/ASM.ma |
---|
133 | ASM/CostsProof.ma: redundant arithmetics/bigops.ma |
---|
134 | RTLabs/RTLabs_partial_traces.ma: redundant RTLabs/CostSpec.ma |
---|