« Up

library-complexity 1.0+8.16 41 m 0 s 🏆

Context

# 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.1      Formal proof management system
dune                  3.12.1      Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        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"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-library-complexity.1.0+8.16 coq.8.16.1
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-library-complexity.1.0+8.16 coq.8.16.1
Return code
0
Duration
26 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-library-complexity.1.0+8.16 coq.8.16.1
Return code
0
Duration
41 m 0 s

Installation size

Total: 60 M

  • 13 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.vo
  • 5 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.glob
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatComp.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TapeDecode.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.glob
  • 957 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/M_LM2TM.vo
  • 849 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT_to_SAT.vo
  • 823 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/mTM_to_singleTapeTM.glob
  • 774 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/LinTimeDecodable.vo
  • 774 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/CompCode.vo
  • 733 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Unfolding.vo
  • 662 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/UnfoldClosBounds.glob
  • 585 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_FlatClique.vo
  • 577 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/M_LM2TM.glob
  • 546 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/ComparisonTimeBoundDerivation.vo
  • 520 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.glob
  • 513 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatCC.vo
  • 457 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/DecodeTape.vo
  • 427 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.vo
  • 421 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm.vo
  • 419 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNP_is_hard.glob
  • 417 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.vo
  • 407 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.glob
  • 404 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatComp.glob
  • 380 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachine.vo
  • 379 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTime.vo
  • 379 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/FlatClique.vo
  • 377 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SAT_inNP.vo
  • 375 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/mTM_to_singleTapeTM.vo
  • 369 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FormulaEncoding.vo
  • 358 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsSub.vo
  • 356 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/UnfoldClosBounds.vo
  • 335 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/LM_to_mTM.vo
  • 326 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/SingleTMGenNP_to_TCC.v
  • 324 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/UnivDecTime.vo
  • 309 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatTCC.vo
  • 307 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/HeapMachine.vo
  • 301 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/M2MBounds.vo
  • 286 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Decompile.vo
  • 276 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNPBool.vo
  • 271 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/M_multi2mono.vo
  • 270 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/Decode.vo
  • 255 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNP_is_hard.vo
  • 254 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT.vo
  • 252 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT_to_SAT.glob
  • 248 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatEnc.vo
  • 246 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsAdd.vo
  • 220 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsCompare.vo
  • 220 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/DecodeTapes.vo
  • 212 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Compile.vo
  • 211 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatFun.vo
  • 209 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/ComparisonTimeBoundDerivation.glob
  • 207 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisUnfoldClos.vo
  • 199 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/MorePrelim.vo
  • 191 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatCC.glob
  • 190 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/NP.vo
  • 190 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FunctionalDefinitions.vo
  • 182 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/CC.vo
  • 181 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/HierarchyTheorem/AbstractTimeHierarchyTheorem.vo
  • 180 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldTailRec.vo
  • 179 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMunflatten.vo
  • 178 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/PTCC_Preludes.vo
  • 178 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP.vo
  • 173 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/FlatFinTypes.vo
  • 172 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LBinNums.vo
  • 169 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/M2MBounds.glob
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMunflatten.glob
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/DecodeList.vo
  • 167 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TCC.vo
  • 166 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_Clique.vo
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisStep.glob
  • 165 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.glob
  • 164 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/LargestVar.vo
  • 164 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/LM_to_mTM.glob
  • 160 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/PolyTimeComputable.vo
  • 158 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_homomorphisms.vo
  • 156 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisStep.vo
  • 155 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_FlatClique.glob
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/BinaryCC.vo
  • 152 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.vo
  • 147 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractSubstMachine.vo
  • 146 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/SpaceBoundsTime.vo
  • 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatSingleTMGenNP_to_FlatTCC.v
  • 141 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SAT_inNP.glob
  • 140 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Lookup.vo
  • 140 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/PolyBounds.vo
  • 138 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.vo
  • 131 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTimeBool.vo
  • 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatFun.glob
  • 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FormulaEncoding.glob
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.vo
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/UpToCPoly.vo
  • 120 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Compound/MoveToSymbol_niceSpec.vo
  • 120 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCode.vo
  • 115 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SubtermProperty.vo
  • 114 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/DecodeTape.glob
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Definitions.vo
  • 110 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/MorePrelim.glob
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/L_to_LM.vo
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/EncodeTapesInvariants.vo
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TM_single.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Shared.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/CC.glob
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.vo
  • 101 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/kSAT.vo
  • 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCodeSpace.vo
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/PolyBounds.glob
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/FlatClique.glob
  • 92 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/HierarchyTheorem/TimeHierarchyTheorem.vo
  • 90 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachine.glob
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_Clique.glob
  • 87 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin.vo
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/PTCC_Preludes.glob
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/kSAT_to_SAT.vo
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/FlatFinTypes.glob
  • 82 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatten.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TCC.glob
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_homomorphisms.glob
  • 80 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatTCC.glob
  • 79 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.vo
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TCC_to_CC.vo
  • 78 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/IterupN.vo
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/LPro.vo
  • 77 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldHeap.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TM_single.glob
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.glob
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/ONotation.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/UniformHomomorphisms.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatEnc.glob
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTime.glob
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/CompCode.glob
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/M_multi2mono.glob
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SAT.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/PrettyBounds.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/LambdaDepth.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Subtypes.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/EncodableP.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/IntermediateProblems.vo
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/FlatUGraph.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/BinaryCC_to_FSAT.v
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/Pigeonhole.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachineDef.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNPBool.glob
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCode.glob
  • 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/HierarchyTheorem/AbstractTimeHierarchyTheorem.glob
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/EncodeTapesInvariants.glob
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP_fixed_mTM.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/PolyTimeComputable.glob
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/SpaceBoundsTime.glob
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LComparison.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm_def.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds.v
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCodeSpace.glob
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/ONotationIsAppropriate.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/Decode.glob
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflat.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/Tactics.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/LMGenNP.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/DecodeBool.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/UpToCPoly.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/NP.glob
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNP.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SharedSAT.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/PSLCompat.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT_to_SAT.v
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisUnfoldClos.glob
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SpaceBounds.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SAT.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/PrettyBounds.glob
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FunctionalDefinitions.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/DecodeTapes.glob
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SizeBounds.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.glob
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LDepPair.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldTailRec.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/DecodeList.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractSubstMachine.glob
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNums.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/Clique.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/M2MBounds.v
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TapeDecode.glob
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatCC.v
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/ONotationIsAppropriate.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Definitions.glob
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachineDef.glob
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Compile.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/UniformHomomorphisms.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/UnivDecTime.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.glob
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/HierarchyTheorem/TimeHierarchyTheorem.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatten.glob
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/ONotation.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SubtermProperty.glob
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_FlatClique.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/ComparisonTimeBoundDerivation.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Unfolding.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/Pigeonhole.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/FlatUGraph.glob
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Monotonic.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.glob
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachine.v
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP.glob
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FormulaEncoding.v
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatCC_to_BinaryCC.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/Tactics.glob
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/DecodeTape.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/UGraph.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/PTCC_Preludes.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/LM_to_mTM.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/kSAT_to_Clique.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SAT_inNP.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatComp.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/MorePrelim.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TCC_to_CC.glob
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/FlatTCC.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/FlatClique.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/LargestVar.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflat.glob
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMunflatten.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/mTM_to_singleTapeTM.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCode.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/kSAT.glob
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/L_to_LM.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LBinNums.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_homomorphisms.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/BinaryCC.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin.glob
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/FlatFinTypes.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsSub.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TCC.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/CompCode.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTimeBool.glob
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/CC.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/SubstMachine.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Subtypes.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/M_multi2mono.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/IterupN.glob
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/UnfoldClosBounds.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/M_LM2TM.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldHeap.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Compound/MoveToSymbol_niceSpec.glob
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/HeapMachine.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/kSAT_to_SAT.glob
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTime.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/Decode.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/PolyTimeComputable.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/HierarchyTheorem/AbstractTimeHierarchyTheorem.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/PolyBounds.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/DecodeList.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsAdd.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/UpToCPoly.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/LMGenNP.glob
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/NP.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatFun.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsCompare.glob
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/DecodeTapes.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/FSAT/FSAT.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/BaseCodeSpace.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/SpaceBoundsTime.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/TM_LHeapInterpreter/LMBounds_Loop.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP_fixed_mTM.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/EncodableP.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/PSLCompat.glob
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisUnfoldClos.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/PrettyBounds.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNP_is_hard.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/LambdaDepth.glob
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/FlatTCC_to_FlatCC.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/ONotation.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatten.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Definitions.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldTailRec.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/TM_single.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNP.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/Pigeonhole.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Monotonic.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SizeBounds.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SubtermProperty.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNPBool.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Decompile.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/Clique.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractSubstMachine.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/CC_to_BinaryCC.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/DecodeBool.glob
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TMGenNP_fixed_singleTapeTM_to_FlatFunSingleTMGenNP.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/CookPrelim/Tactics.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FunctionalDefinitions.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/SizeAnalysisStep.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm_def.glob
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/IterupN.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/UnivDecTime.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SAT.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/UniformHomomorphisms.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Reductions/TCC_to_CC.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/SingleTMGenNP.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/ONotationIsAppropriate.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Compile.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/FlatUGraph.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/HierarchyTheorem/TimeHierarchyTheorem.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Shared.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/LinTimeDecodable.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SharedSAT.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflatEnc.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Unfolding.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SpaceBounds.glob
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LBinNums.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Single/EncodeTapesInvariants.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsSub.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Lookup.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/kSAT.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/L_to_LM.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/UnfoldHeap.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Compound/MoveToSymbol_niceSpec.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/CookLevin/Subproblems/BinaryCC.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TMflat.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/LPro.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/AbstractHeapMachineDef.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/LargestVar.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LDepPair.glob
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Monotonic.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/EvalForTimeBool.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/Subtypes.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/HeapMachine.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/EncodableP.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SpaceBounds.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Libs/PSLCompat.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/UGraph.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/TM/TapeDecode.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsAdd.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/kSAT_to_SAT.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/IntermediateProblems.glob
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/IntermediateProblems.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/TM/TMGenNP_fixed_mTM.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/SubstMachine.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNumsCompare.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/Code/DecodeBool.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/Clique.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/TM/PrettyBounds/SizeBounds.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/LambdaDepth.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/LMGenNP.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/CanEnumTerm_def.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/Complexity/LinTimeDecodable.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/L/GenNP.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/Decompile.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LDepPair.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/FlatPro/Computable/LPro.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Shared.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/SAT/SharedSAT.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/Lookup.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LComparison.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/NP/Clique/UGraph.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Datatypes/LComparison.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNums.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/AbstractMachines/Computable/SubstMachine.glob
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Complexity/L/Functions/BinNums.v

Uninstall 🧹

Command
opam remove -y coq-library-complexity.1.0+8.16
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣