# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-findutils 1 Virtual package relying on findutils
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq 8.16.0 Formal proof management system
dune 3.6.2 Fast, portable, and opinionated build system
ocaml 4.10.2 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2 Official release 4.10.2
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.9.5 A library manager for OCaml
zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "forster@cs.uni-saarland.de"
homepage: "https://github.com/uds-psl/coq-library-complexity/"
dev-repo: "git+https://github.com/uds-psl/coq-library-complexity/"
bug-reports: "https://github.com/uds-psl/coq-library-complexity/issues"
authors: ["Fabian Kunze"
"Lennard Gäher"
"Maximilian Wuttke"
"Yannick Forster"
"Stefan Haan"]
synopsis: "A Coq Library of Complexity Theory"
license: "CECILL-2.1"
build: [
[make "-j%{jobs}%"]
]
install: [
[make "install"]
]
depends: [
"coq" {>= "8.16" & < "8.17"}
"coq-library-undecidability" {= "1.0.1+8.16" }
]
url {
src: "https://github.com/uds-psl/coq-library-complexity/archive/refs/tags/v1.0+8.16.tar.gz"
checksum: "sha256=f07ca356e7b3ebb03ac6ccc07a3e389dab293ec01b1994027597998859f97306"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-library-complexity.1.0+8.16 coq.8.16.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-library-complexity.1.0+8.16 coq.8.16.0opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-library-complexity.1.0+8.16 coq.8.16.0Total: 60 M
../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatComp.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TapeDecode.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/M_LM2TM.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT_to_SAT.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/mTM_to_singleTapeTM.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/LinTimeDecodable.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/CompCode.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Unfolding.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/UnfoldClosBounds.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_FlatClique.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/M_LM2TM.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/ComparisonTimeBoundDerivation.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/DecodeTape.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNP_is_hard.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatComp.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachine.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTime.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/FlatClique.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SAT_inNP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/mTM_to_singleTapeTM.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FormulaEncoding.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsSub.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/UnfoldClosBounds.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/LM_to_mTM.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/UnivDecTime.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatTCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/HeapMachine.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/M2MBounds.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Decompile.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNPBool.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/M_multi2mono.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/Decode.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNP_is_hard.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT_to_SAT.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatEnc.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsAdd.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsCompare.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/DecodeTapes.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Compile.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatFun.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/ComparisonTimeBoundDerivation.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisUnfoldClos.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/MorePrelim.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/NP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FunctionalDefinitions.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/CC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/HierarchyTheorem/AbstractTimeHierarchyTheorem.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldTailRec.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMunflatten.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/PTCC_Preludes.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/FlatFinTypes.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LBinNums.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/M2MBounds.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMunflatten.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/DecodeList.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_Clique.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisStep.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/LargestVar.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/LM_to_mTM.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/PolyTimeComputable.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_homomorphisms.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisStep.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_FlatClique.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/BinaryCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractSubstMachine.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/SpaceBoundsTime.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SAT_inNP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Lookup.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/PolyBounds.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTimeBool.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatFun.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FormulaEncoding.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/UpToCPoly.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Compound/MoveToSymbol_niceSpec.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCode.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SubtermProperty.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/DecodeTape.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Definitions.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/MorePrelim.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/L_to_LM.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/EncodeTapesInvariants.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TM_single.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Shared.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/CC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/kSAT.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCodeSpace.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/PolyBounds.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/FlatClique.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/HierarchyTheorem/TimeHierarchyTheorem.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachine.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_Clique.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/PTCC_Preludes.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/kSAT_to_SAT.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/FlatFinTypes.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatten.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_homomorphisms.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatTCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TCC_to_CC.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/IterupN.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/LPro.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldHeap.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TM_single.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/ONotation.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/UniformHomomorphisms.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatEnc.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTime.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/CompCode.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/M_multi2mono.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SAT.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/PrettyBounds.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/LambdaDepth.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Subtypes.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/EncodableP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/IntermediateProblems.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/FlatUGraph.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/Pigeonhole.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachineDef.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNPBool.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCode.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/HierarchyTheorem/AbstractTimeHierarchyTheorem.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/EncodeTapesInvariants.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP_fixed_mTM.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/PolyTimeComputable.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/SpaceBoundsTime.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LComparison.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm_def.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCodeSpace.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/ONotationIsAppropriate.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/Decode.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflat.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/Tactics.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/LMGenNP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/DecodeBool.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/UpToCPoly.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/NP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNP.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SharedSAT.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/PSLCompat.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT_to_SAT.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisUnfoldClos.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SpaceBounds.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SAT.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/PrettyBounds.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FunctionalDefinitions.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/DecodeTapes.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SizeBounds.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LDepPair.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldTailRec.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/DecodeList.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractSubstMachine.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNums.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/Clique.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/M2MBounds.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TapeDecode.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/ONotationIsAppropriate.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Definitions.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachineDef.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Compile.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/UniformHomomorphisms.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/UnivDecTime.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/HierarchyTheorem/TimeHierarchyTheorem.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatten.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/ONotation.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SubtermProperty.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_FlatClique.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/ComparisonTimeBoundDerivation.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Unfolding.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/Pigeonhole.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/FlatUGraph.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Monotonic.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachine.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FormulaEncoding.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/Tactics.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/DecodeTape.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/UGraph.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/PTCC_Preludes.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/LM_to_mTM.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_Clique.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SAT_inNP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatComp.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/MorePrelim.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TCC_to_CC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatTCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/FlatClique.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/LargestVar.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflat.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMunflatten.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/mTM_to_singleTapeTM.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCode.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/kSAT.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/L_to_LM.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LBinNums.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_homomorphisms.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/BinaryCC.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/FlatFinTypes.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsSub.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/CompCode.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTimeBool.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/CC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/SubstMachine.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Subtypes.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/M_multi2mono.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/IterupN.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/UnfoldClosBounds.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/M_LM2TM.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldHeap.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Compound/MoveToSymbol_niceSpec.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/HeapMachine.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/kSAT_to_SAT.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTime.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/Decode.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/PolyTimeComputable.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/HierarchyTheorem/AbstractTimeHierarchyTheorem.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/PolyBounds.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/DecodeList.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsAdd.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/UpToCPoly.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/LMGenNP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/NP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatFun.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsCompare.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/DecodeTapes.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCodeSpace.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/SpaceBoundsTime.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP_fixed_mTM.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/EncodableP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/PSLCompat.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisUnfoldClos.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/PrettyBounds.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNP_is_hard.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/LambdaDepth.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/ONotation.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatten.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Definitions.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldTailRec.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TM_single.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNP.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/Pigeonhole.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Monotonic.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SizeBounds.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SubtermProperty.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNPBool.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Decompile.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/Clique.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractSubstMachine.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/DecodeBool.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/CookPrelim/Tactics.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FunctionalDefinitions.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisStep.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm_def.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/IterupN.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/UnivDecTime.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SAT.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/UniformHomomorphisms.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TCC_to_CC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/ONotationIsAppropriate.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Compile.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/FlatUGraph.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/HierarchyTheorem/TimeHierarchyTheorem.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Shared.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/LinTimeDecodable.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SharedSAT.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflatEnc.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Unfolding.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SpaceBounds.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LBinNums.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Single/EncodeTapesInvariants.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsSub.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Lookup.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/kSAT.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/L_to_LM.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldHeap.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Compound/MoveToSymbol_niceSpec.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/BinaryCC.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TMflat.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/LPro.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachineDef.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/LargestVar.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LDepPair.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Monotonic.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTimeBool.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/Subtypes.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/HeapMachine.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/EncodableP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SpaceBounds.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Libs/PSLCompat.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/UGraph.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/TM/TapeDecode.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsAdd.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/kSAT_to_SAT.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/IntermediateProblems.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/IntermediateProblems.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP_fixed_mTM.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/SubstMachine.vo../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNumsCompare.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/Code/DecodeBool.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/Clique.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SizeBounds.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/LambdaDepth.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/LMGenNP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm_def.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/Complexity/LinTimeDecodable.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/L/GenNP.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Decompile.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LDepPair.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/LPro.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Shared.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/SAT/SharedSAT.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Lookup.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LComparison.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/NP/Clique/UGraph.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Datatypes/LComparison.v../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNums.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/SubstMachine.glob../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/Complexity/L/Functions/BinNums.vopam remove -y coq-library-complexity.1.0+8.16