utilities/extralib.ma: redundant basics/lists/list.ma
utilities/extralib.ma: redundant basics/types.ma
utilities/monad.ma: redundant basics/relations.ma
utilities/monad.ma: redundant basics/types.ma
utilities/option.ma: redundant basics/types.ma
utilities/extranat.ma: redundant basics/types.ma
ASM/Vector.ma: redundant arithmetics/nat.ma
ASM/Vector.ma: redundant basics/types.ma
ASM/Vector.ma: redundant basics/lists/list.ma
ASM/BitVector.ma: redundant arithmetics/nat.ma
common/PositiveMap.ma: redundant basics/types.ma
common/Errors.ma: redundant utilities/monad.ma
common/Errors.ma: redundant basics/russell.ma
common/Errors.ma: redundant basics/lists/list.ma
common/Errors.ma: redundant basics/logic.ma
common/Errors.ma: redundant basics/types.ma
utilities/lists.ma: redundant utilities/monad.ma
utilities/lists.ma: redundant utilities/option.ma
utilities/lists.ma: redundant basics/lists/list.ma
common/Identifiers.ma: redundant utilities/binary/positive.ma
common/Identifiers.ma: redundant basics/types.ma
common/Integers.ma: redundant ASM/BitVector.ma
common/Integers.ma: redundant utilities/extranat.ma
common/Integers.ma: redundant arithmetics/nat.ma
common/AST.ma: redundant basics/types.ma
ASM/BitVectorZ.ma: redundant ASM/BitVector.ma
ASM/BitVectorZ.ma: redundant utilities/binary/Z.ma
common/Values.ma: redundant common/Errors.ma
utilities/Coqlib.ma: redundant basics/lists/list.ma
utilities/Coqlib.ma: redundant basics/types.ma
common/GenMem.ma: redundant common/Pointers.ma
common/GenMem.ma: redundant utilities/extralib.ma
common/Globalenvs.ma: redundant common/AST.ma
common/Globalenvs.ma: redundant common/Errors.ma
common/extraGlobalenvs.ma: redundant common/AST.ma
common/ExtraMonads.ma: redundant common/Errors.ma
utilities/bind_new.ma: redundant utilities/monad.ma
common/LabelledObjects.ma: redundant utilities/lists.ma
joint/Joint.ma: redundant utilities/lists.ma
common/Graphs.ma: redundant common/Identifiers.ma
ASM/BitVectorTrie.ma: redundant basics/types.ma
common/Graphs.ma: redundant basics/types.ma
ASM/I8051.ma: redundant arithmetics/nat.ma
joint/TranslateUtils.ma: redundant joint/Joint.ma
joint/semanticsUtils.ma: redundant ASM/BitVectorTrie.ma
joint/semanticsUtils.ma: redundant utilities/hide.ma
joint/BEMem.ma: redundant common/ByteValues.ma
common/Events.ma: redundant utilities/extralib.ma
common/Events.ma: redundant basics/lists/list.ma
joint/joint_semantics.ma: redundant common/Globalenvs.ma
common/StructuredTraces.ma: redundant utilities/option.ma
common/StructuredTraces.ma: redundant common/CostLabel.ma
common/StructuredTraces.ma: redundant basics/bool.ma
joint/semantics_blocks.ma: redundant joint/blocks.ma
common/Animation.ma: redundant arithmetics/nat.ma
common/SmallstepExec.ma: redundant common/Integers.ma
common/SmallstepExec.ma: redundant utilities/extralib.ma
Clight/Csyntax.ma: redundant common/Errors.ma
Clight/Csem.ma: redundant Clight/Csyntax.ma
Clight/Cexec.ma: redundant utilities/extralib.ma
ERTLptr/ERTLptr_semantics.ma: redundant joint/semanticsUtils.ma
Clight/frontend_misc.ma: redundant common/IOMonad.ma
Clight/frontend_misc.ma: redundant common/Pointers.ma
Clight/frontend_misc.ma: redundant Clight/TypeComparison.ma
Clight/MemProperties.ma: redundant common/FrontEndMem.ma
Clight/switchRemoval.ma: redundant utilities/extralib.ma
Clight/switchRemoval.ma: redundant common/Identifiers.ma
Clight/switchRemoval.ma: redundant basics/lists/listb.ma
RTLabs/RTLabs_syntax.ma: redundant ASM/Vector.ma
common/FrontEndOps.ma: redundant common/Values.ma
RTLabs/RTLabs_syntax.ma: redundant common/AST.ma
RTLabs/RTLabs_syntax.ma: redundant basics/logic.ma
RTLabs/CostCheck.ma: redundant RTLabs/CostSpec.ma
RTLabs/RTLabs_semantics.ma: redundant common/Errors.ma
RTLabs/RTLabs_semantics.ma: redundant basics/lists/list.ma
Cminor/toRTLabs.ma: redundant Cminor/Cminor_syntax.ma
Cminor/toRTLabs.ma: redundant common/Globalenvs.ma
Cminor/toRTLabs.ma: redundant utilities/lists.ma
Cminor/Cminor_semantics.ma: redundant common/FrontEndMem.ma
Cminor/Cminor_semantics.ma: redundant common/Events.ma
Clight/toCminor.ma: redundant basics/lists/list.ma
Clight/SimplifyCasts.ma: redundant Clight/Cexec.ma
Clight/SimplifyCasts.ma: redundant Clight/TypeComparison.ma
Clight/SimplifyCasts.ma: redundant Clight/Csyntax.ma
ASM/UtilBranch.ma: redundant ASM/Util.ma
ERTL/ERTLToERTLptr.ma: redundant ERTL/ERTL.ma
RTLabs/RTLabs_traces.ma: redundant RTLabs/CostSpec.ma
joint/extra_joint_semantics.ma: redundant joint/joint_semantics.ma
ERTL/ERTLtoERTLptrUtils.ma: redundant common/ExtraMonads.ma
ERTL/ERTLtoERTLptrUtils.ma: redundant joint/Traces.ma
joint/StatusSimulationHelper.ma: redundant joint/Traces.ma
joint/StatusSimulationHelper.ma: redundant joint/semanticsUtils.ma
common/stacksize.ma: redundant basics/lists/list.ma
ASM/Fetch.ma: redundant ASM/Arithmetic.ma
ASM/Assembly.ma: redundant ASM/Arithmetic.ma
ASM/Assembly.ma: redundant ASM/ASM.ma
semantics.ma: redundant ERTL/ERTL_semantics.ma
compiler.ma: redundant ASM/ASMCosts.ma
ASM/PolicyFront.ma: redundant utilities/extralib.ma
ASM/PolicyFront.ma: redundant ASM/Status.ma
ASM/PolicyFront.ma: redundant ASM/Fetch.ma
ASM/PolicyFront.ma: redundant ASM/Arithmetic.ma
ASM/PolicyFront.ma: redundant ASM/ASM.ma
LIN/LINToASM.ma: redundant ASM/Util.ma
ERTLptr/ERTLptrToLTL.ma: redundant ASM/Arithmetic.ma
utilities/adt/set_adt.ma: redundant arithmetics/nat.ma
utilities/adt/set_adt.ma: redundant basics/lists/list.ma
utilities/adt/set_adt.ma: redundant basics/types.ma
ERTLptr/liveness.ma: redundant ASM/Util.ma
RTL/RTLToERTL.ma: redundant common/Identifiers.ma
RTLabs/RTLabsToRTL.ma: redundant common/Graphs.ma
Clight/test/search.test.ma: redundant common/Animation.ma
Clight/toCminorOps.ma: redundant Clight/frontend_misc.ma
Clight/toCminorOps.ma: redundant Clight/Cexec.ma
Clight/toCminorCorrectnessExpr.ma: redundant common/Globalenvs.ma
Clight/toCminorCorrectnessExpr.ma: redundant Clight/toCminor.ma
Clight/toCminorCorrectness.ma: redundant Cminor/Cminor_abstract.ma
Clight/toCminorCorrectness.ma: redundant Clight/Clight_abstract.ma
Clight/toCminorCorrectness.ma: redundant Clight/memoryInjections.ma
Clight/toCminorCorrectness.ma: redundant common/Globalenvs.ma
Clight/toCminorCorrectness.ma: redundant Clight/CexecInd.ma
Clight/toCminorCorrectness.ma: redundant Clight/toCminor.ma
utilities/adt/priority_set_adt.ma: redundant arithmetics/nat.ma
utilities/adt/priority_set_adt.ma: redundant basics/lists/list.ma
utilities/adt/priority_set_adt.ma: redundant basics/types.ma
ASM/Test.ma: redundant ASM/StatusProofs.ma
ASM/Test.ma: redundant ASM/Interpret.ma
ASM/Test.ma: redundant ASM/Assembly.ma
ERTLptr/ERTLptrToLTLProof.ma: redundant common/StatusSimulation.ma
ERTLptr/ERTLptrToLTLProof.ma: redundant joint/Traces.ma
Clight/test/castremoval.test.ma: redundant common/Animation.ma
ASM/WellLabeled.ma: redundant ASM/ASM.ma
ASM/CostsProof.ma: redundant arithmetics/bigops.ma
RTLabs/RTLabs_partial_traces.ma: redundant RTLabs/CostSpec.ma