ยซ Up

tactician-stdlib dev 48 m 2 s ๐Ÿ†

๐Ÿ“… (2022-05-24 01:37:32 UTC)

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                 dev         Formal proof management system
dune                3.1.1       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.3       A library manager for OCaml
zarith              1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
name: "coq-tactician-stdlib"
synopsis: "Recompiles Coq's standard libary with Tactician's instrumentation loaded"
description: """
  *** WARNING *** This package will overwrite Coq's standard library files.
  This package recompiles Coq's standard library with Tactician's (`coq-tactician`)
  instrumentation loaded such that Tactician can learn from the library. When you
  install this package, the current `.vo` files of the standard library are backed
  in the folder `user-contrib/Tactician/stdlib-backup`. The new `.vo` files are
  equivalent to the originals, except that they also contain Tactician's tactic
  databases. After installation of this package, all other Coq developments that
  are installed will also need to be recompiled. The 'tactician recompile' command
  line utility can help with this.
  Upon removal of this package, the original files will be placed back.
"""
homepage: "https://coq-tactician.github.io"
dev-repo: "git+https://github.com/coq-tactician/coq-tactician-stdlib"
bug-reports: "https://github.com/coq-tactician/coq-tactician-stdlib/issues"
maintainer: "Lasse Blaauwbroek <lasse@blaauwbroek.eu>"
authors: "Lasse Blaauwbroek <lasse@blaauwbroek.eu"
messages: [
  "*** WARNING ***"
  "This package will overwrite Coq's standard library files."
  "A backup of the original files will be placed under Coq's"
  "library directory at user-contrib/tactician-stdlib-backup/"
  "and they will be restored when you remove this package."
  "After installation of this package, all other Coq packages"
  "also need to be recompiled. Running the 'tactician recompile'"
  "command-line utility will help with this process."
]
post-messages: ["
--- The standard library was successfully recompiled ---
In order to finish the process, you should run
tactician recompile
" {success}]
depends: [
  "coq" {= "dev"}
  "coq-tactician"
]
build: [
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
remove: [
  [make "restore"]
]
url {
  src: "git+https://github.com/coq-tactician/coq-tactician-stdlib.git#coqdev"
}
tags: [
  "keyword:tactic-learning"
  "keyword:machine-learning"
  "keyword:automation"
  "keyword:proof-synthesis"
  "category:Miscellaneous/Coq Extensions"
  "logpath:Tactician"
]

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-tactician-stdlib.dev coq.dev
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-tactician-stdlib.dev coq.dev
Return code
0
Duration
19 m 14 s

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y coq-tactician-stdlib.dev coq.dev
Return code
0
Duration
48 m 2 s

Installation size

Total: 53 M

  • 4 M ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapAVL.vo
  • 3 M ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapFullAVL.vo
  • 1 M ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersEx.vo
  • 1 M ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetRBT.vo
  • 856 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetAVL.vo
  • 752 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapList.vo
  • 616 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/BinInt.vo
  • 502 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetAVL.vo
  • 495 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/Byte.vo
  • 480 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Field_theory.vo
  • 476 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapFacts.vo
  • 466 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/List.vo
  • 448 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Hexadecimal.vo
  • 430 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/BinNat.vo
  • 418 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZBits.vo
  • 414 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/PeanoNat.vo
  • 411 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int31/Cyclic31.vo
  • 401 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZProperties.vo
  • 389 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetList.vo
  • 367 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapWeakList.vo
  • 365 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalString.vo
  • 344 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_polynom.vo
  • 343 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NBits.vo
  • 340 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/BinPos.vo
  • 334 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetProperties.vo
  • 330 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
  • 326 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetProperties.vo
  • 317 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NProperties.vo
  • 316 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Tauto.vo
  • 314 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrbool.vo
  • 302 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RiemannInt_SF.vo
  • 300 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetGenTree.vo
  • 290 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RiemannInt.vo
  • 290 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/Ascii.vo
  • 289 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/Uint63.vo
  • 286 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetInterface.vo
  • 276 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ratan.vo
  • 271 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZLcm.vo
  • 259 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalFacts.vo
  • 257 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZLog.vo
  • 254 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalString.vo
  • 254 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/EnvRing.vo
  • 239 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/RingMicromega.vo
  • 238 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZDivEucl.vo
  • 234 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetEqProperties.vo
  • 226 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetEqProperties.vo
  • 225 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZMicromega.vo
  • 225 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Binary/ZBinary.vo
  • 217 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZDivTrunc.vo
  • 209 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZDivFloor.vo
  • 207 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZSqrt.vo
  • 200 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetPositive.vo
  • 198 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapPositive.vo
  • 196 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Peano/NPeano.vo
  • 191 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring_polynom.vo
  • 190 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Decimal.vo
  • 190 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NLcm.vo
  • 189 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetCompat.vo
  • 187 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalPos.vo
  • 187 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetPositive.vo
  • 186 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.vo
  • 186 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RIneq.vo
  • 184 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/POrderedType.vo
  • 183 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Binary/NBinary.vo
  • 182 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis5.vo
  • 179 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/SetoidList.vo
  • 176 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalFacts.vo
  • 175 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZGcd.vo
  • 174 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/GenericMinMax.vo
  • 174 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NDefOps.vo
  • 171 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/QArith_base.vo
  • 169 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZPow.vo
  • 168 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo1.vo
  • 167 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NGcd.vo
  • 164 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Permutation.vo
  • 163 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NLog.vo
  • 163 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetList.vo
  • 160 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Specif.vo
  • 160 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Logic.vo
  • 158 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalQ.vo
  • 157 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/NatPairs/ZNatPairs.vo
  • 154 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetDecide.vo
  • 153 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtopology.vo
  • 153 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetDecide.vo
  • 152 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Byte.vo
  • 149 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NDiv.vo
  • 149 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NPow.vo
  • 146 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveRealsMorphisms.vo
  • 146 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/btauto/Algebra.vo
  • 146 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalQ.vo
  • 145 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/InitialRing.vo
  • 141 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_theory.vo
  • 140 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
  • 140 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis_reg.vo
  • 139 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZPow.vo
  • 139 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetWeakList.vo
  • 139 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NParity.vo
  • 139 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NSqrt.vo
  • 139 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZDiv.vo
  • 139 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZParity.vo
  • 138 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveReals.vo
  • 135 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetToFiniteSet.vo
  • 135 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZAxioms.vo
  • 135 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/ZModulo/ZModulo.vo
  • 135 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ChoiceFacts.vo
  • 134 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetToFiniteSet.vo
  • 132 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetFacts.vo
  • 131 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NSub.vo
  • 131 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZMulOrder.vo
  • 131 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis1.vo
  • 130 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NIso.vo
  • 130 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetBridge.vo
  • 129 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZMaxMin.vo
  • 127 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NStrongRec.vo
  • 124 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveCauchyReals.vo
  • 123 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ClassicalDedekindReals.vo
  • 123 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveRcomplete.vo
  • 121 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/VectorSpec.vo
  • 121 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring_initial.vo
  • 121 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalNat.vo
  • 120 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveCauchyAbs.vo
  • 120 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetFacts.vo
  • 119 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NMaxMin.vo
  • 119 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalR.vo
  • 118 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZGcd.vo
  • 117 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatLemmas.vo
  • 117 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalR.vo
  • 115 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZAddOrder.vo
  • 114 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring.vo
  • 113 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalPos.vo
  • 112 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Znumtheory.vo
  • 111 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Cring.vo
  • 110 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrderedTypeEx.vo
  • 110 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZParity.vo
  • 107 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NAxioms.vo
  • 104 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZMulOrder.vo
  • 103 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/OrderedRing.vo
  • 102 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NMulOrder.vo
  • 101 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NOrder.vo
  • 100 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/EquivDec.vo
  • 98 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/NewtonInt.vo
  • 98 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/Vector.vo
  • 97 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZAdd.vo
  • 97 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rpower.vo
  • 97 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Runcountable.vo
  • 96 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/PSeries_reg.vo
  • 96 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetWeakList.vo
  • 96 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZLt.vo
  • 96 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/nsatz/NsatzTactic.vo
  • 95 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SeqProp.vo
  • 95 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NAddOrder.vo
  • 95 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveMinMax.vo
  • 94 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rfunctions.vo
  • 92 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Exp_prop.vo
  • 91 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrderedType.vo
  • 90 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersFacts.vo
  • 90 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Znat.vo
  • 90 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zdiv.vo
  • 89 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cos_plus.vo
  • 89 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring_tac.vo
  • 88 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZMul.vo
  • 88 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/PermutSetoid.vo
  • 88 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndigits.vo
  • 87 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/CMorphisms.vo
  • 86 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NAdd.vo
  • 84 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveSum.vo
  • 83 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NBase.vo
  • 82 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/Orders.vo
  • 82 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalNat.vo
  • 81 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveLUB.vo
  • 81 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Int.vo
  • 80 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RList.vo
  • 80 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZDomain.vo
  • 79 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zquot.vo
  • 78 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetInterface.vo
  • 78 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/RMicromega.vo
  • 78 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyInst.vo
  • 77 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrfun.vo
  • 77 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rdefinitions.vo
  • 77 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveLimits.vo
  • 77 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/String.vo
  • 77 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Field_tac.vo
  • 76 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Lexicographic_Product.vo
  • 75 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/MVT.vo
  • 74 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qcanon.vo
  • 74 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Morphisms.vo
  • 73 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZBase.vo
  • 72 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZAxioms.vo
  • 72 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Bool.vo
  • 71 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qpower.vo
  • 70 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/rtauto/Bintree.vo
  • 69 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rderiv.vo
  • 69 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rsqrt_def.vo
  • 69 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Alembert.vo
  • 68 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rlimit.vo
  • 67 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/PartSum.vo
  • 67 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/Cyclic63.vo
  • 66 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis3.vo
  • 65 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rbasic_fun.vo
  • 65 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/CPermutation.vo
  • 65 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rprod.vo
  • 65 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis2.vo
  • 65 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/R_Ifp.vo
  • 65 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapInterface.vo
  • 64 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cos_rel.vo
  • 64 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersTac.vo
  • 63 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zgcd_alt.vo
  • 62 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/VectorDef.vo
  • 62 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/RelationClasses.vo
  • 62 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/Sint63.vo
  • 62 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZOrder.vo
  • 62 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rminmax.vo
  • 62 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZAddOrder.vo
  • 62 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ClassicalConstructiveReals.vo
  • 61 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Raxioms.vo
  • 61 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/SpecFloat.vo
  • 61 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Notations.vo
  • 60 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_reg.vo
  • 60 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/EqualitiesFacts.vo
  • 60 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/SetoidDec.vo
  • 59 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_alt.vo
  • 59 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/CRelationClasses.vo
  • 59 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
  • 59 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int31/Int31.vo
  • 58 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/R_sqrt.vo
  • 58 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/rtauto/Rtauto.vo
  • 58 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/BinPosDef.vo
  • 57 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/FinFun.vo
  • 57 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/QExtra.vo
  • 57 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalZ.vo
  • 56 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_tac.vo
  • 56 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_calc.vo
  • 56 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rseries.vo
  • 56 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Datatypes.vo
  • 55 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SeqSeries.vo
  • 55 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy_prod.vo
  • 54 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Heap.vo
  • 54 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Machin.vo
  • 54 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/btauto/Reflect.vo
  • 54 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_def.vo
  • 53 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/BinIntDef.vo
  • 53 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Arith_prebase.vo
  • 53 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zorder.vo
  • 53 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis4.vo
  • 52 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/HexString.vo
  • 52 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/AltSeries.vo
  • 52 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/Equalities.vo
  • 52 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveAbs.vo
  • 52 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/Fin.vo
  • 51 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/ListSet.vo
  • 50 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpow_facts.vo
  • 50 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Equality.vo
  • 49 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalFacts.vo
  • 49 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpower.vo
  • 48 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Even.vo
  • 48 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/WKL.vo
  • 48 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/PermutEq.vo
  • 48 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zeuclid.vo
  • 48 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Hurkens.vo
  • 48 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Relation_Operators.vo
  • 48 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_facts.vo
  • 47 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Sqrt_reg.vo
  • 47 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssreflect.vo
  • 47 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qminmax.vo
  • 47 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qreals.vo
  • 47 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zdigits.vo
  • 46 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructivePower.vo
  • 46 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Lexicographic_Exponentiation.vo
  • 46 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/QMicromega.vo
  • 46 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZCoeff.vo
  • 45 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rgeom.vo
  • 45 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rsigma.vo
  • 45 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/DecidableTypeEx.vo
  • 44 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Binomial.vo
  • 44 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifySint63.vo
  • 44 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/omega/OmegaLemmas.vo
  • 44 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/R_sqr.vo
  • 43 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/omega/PreOmega.vo
  • 43 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/Pnat.vo
  • 43 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/SetoidPermutation.vo
  • 42 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/nsatz/Nsatz.vo
  • 42 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ConstructiveEpsilon.vo
  • 42 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalZ.vo
  • 41 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qabs.vo
  • 41 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyUint63.vo
  • 41 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/EqdepFacts.vo
  • 40 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ROrderedType.vo
  • 40 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Rings_R.vo
  • 40 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersLists.vo
  • 40 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndec.vo
  • 40 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zeven.vo
  • 39 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndist.vo
  • 39 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyClasses.vo
  • 39 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyBool.vo
  • 38 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/RealField.vo
  • 38 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qreduction.vo
  • 38 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZProperties.vo
  • 37 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/BinNatDef.vo
  • 37 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersAlt.vo
  • 36 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Tactics.vo
  • 36 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ArithProp.vo
  • 36 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Mergesort.vo
  • 36 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/OctalString.vo
  • 36 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Adjointification.vo
  • 36 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Integral_domain.vo
  • 36 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/ZArith_dec.vo
  • 35 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyComparison.vo
  • 35 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZBits.vo
  • 35 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int31/Ring31.vo
  • 35 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rlogic.vo
  • 34 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rcomplete.vo
  • 33 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Nnat.vo
  • 32 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Cantor.vo
  • 31 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrderedTypeAlt.vo
  • 31 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_fun.vo
  • 31 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/FunctionalExtensionality.vo
  • 31 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Sorted.vo
  • 31 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/CEquivalence.vo
  • 30 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Nat.vo
  • 30 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/RelationPairs.vo
  • 30 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Diaconescu.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Powerset_facts.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/DecidableType.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Tactics.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zbool.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qround.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/Ring63.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/QOrderedType.vo
  • 29 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Finite_sets_facts.vo
  • 28 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qcabs.vo
  • 28 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalN.vo
  • 28 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/DecidableClass.vo
  • 28 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qfield.vo
  • 28 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Between.vo
  • 28 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Powerset_Classical_facts.vo
  • 28 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Psatz.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalN.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Lra.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/DiscrR.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatAxioms.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Reals.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Ztac.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Integration.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Compare_dec.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Array/PArray.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/BinaryString.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zwf.vo
  • 27 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Wf_nat.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Fourier_util.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zcomplements.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/ByteVector.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Cpo.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Multiset.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Equivalence.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Wf_Z.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOCamlFloats.vo
  • 26 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatOps.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Infinite_sets.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zcompare.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellString.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveExtra.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/SetoidClass.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Operators_Properties.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Rings_Q.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlNativeString.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZArith_hints.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Ltac.vo
  • 25 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlZBigInt.vo
  • 24 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Refl.vo
  • 24 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlChar.vo
  • 24 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZMul.vo
  • 24 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Image.vo
  • 24 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/Floats.vo
  • 24 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlIntConv.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/PosExtra.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/MExtraction.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Morphisms_Prop.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NaryFunctions.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Eqdep_dec.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Fourier.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rregisternames.vo
  • 23 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SplitAbsolu.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/VectorEq.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Euclid.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Lqa.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Peano.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalEpsilon.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SplitRmult.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Lia.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSets.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZAdd.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlZInt.vo
  • 22 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOCamlInt63.vo
  • 21 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rpow_def.vo
  • 21 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rbase.vo
  • 21 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSets.vo
  • 21 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Plus.vo
  • 21 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Env.vo
  • 21 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Rings_Z.vo
  • 21 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Number.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/ArithRing.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Ensembles.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/DeclConstant.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zhints.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMaps.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/Streams.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/auxiliary.vo
  • 20 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOCamlPArray.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellZInteger.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellZInt.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/WeakFan.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellZNum.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/VarMap.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/ZArithRing.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalDescription.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/ListDec.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/btauto/Btauto.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/SetoidTactics.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zabs.vo
  • 19 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/Coq813.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/ZArith.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Epsilon.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Wf.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Uniset.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpow_alt.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Div2.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Morphisms_Relations.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyNat.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyN.vo
  • 18 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Mult.vo
  • 17 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Integers.vo
  • 17 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalChoice.vo
  • 17 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Decidable.vo
  • 17 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Bvector.vo
  • 17 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/SetoidChoice.vo
  • 16 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/NArithRing.vo
  • 16 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/ZArith_base.vo
  • 16 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Classical_Prop.vo
  • 16 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Zerob.vo
  • 16 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlNatBigInt.vo
  • 16 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/BinList.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/StreamMemo.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Classical_sets.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/IndefiniteDescription.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/EqNat.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zmin.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Powerset.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Zify.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlNatInt.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zmax.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/QArith.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellNatNum.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/ListTactics.vo
  • 15 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/NArith.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qring.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Lt.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Peano_dec.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Abstract/DoubleType.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ExtensionalityFacts.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Tauto.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Description.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Gt.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Wf.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Field.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/List.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/funind/Recdef.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlString.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/BoolOrder.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/JMeq.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellNatInteger.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellNatInt.vo
  • 14 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyPow.vo
  • 13 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_base.vo
  • 13 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zmisc.vo
  • 13 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpow_def.vo
  • 13 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Relation_Definitions.vo
  • 13 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Arith.vo
  • 13 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Std.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Minus.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Constructive_sets.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Bool_nat.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalUniqueChoice.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Compare.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZBase.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zminmax.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Berardi.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Arith_base.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/HLevels.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_3_facts.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_1.vo
  • 12 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Max.vo
  • 11 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Subset.vo
  • 11 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/PrimFloat.vo
  • 11 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Le.vo
  • 11 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Classical_Pred_Type.vo
  • 11 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Program.vo
  • 11 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_2_facts.vo
  • 11 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Partial_Order.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndiv_def.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Factorial.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Min.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Syntax.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Well_Ordering.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Algebra_syntax.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_2.vo
  • 10 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Sorting.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Notations.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/PropExtensionality.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ngcd_def.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Wellfounded.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Classical.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Array.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Nsqrt_def.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/PArith.vo
  • 9 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Finite_sets.vo
  • 8 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Sumbool.vo
  • 8 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Setoids/Setoid.vo
  • 8 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_1_facts.vo
  • 8 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/PrimInt63.vo
  • 8 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Combinators.vo
  • 7 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/BinNums.vo
  • 7 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/StrictProp.vo
  • 7 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_3.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/BoolEq.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/PropExtensionalityFacts.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Disjoint_Union.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ProofIrrelevanceFacts.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/IfProp.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Permut.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Constr.vo
  • 6 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Union.vo
  • 5 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrunder.vo
  • 5 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Transitive_Closure.vo
  • 5 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Pattern.vo
  • 5 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ProofIrrelevance.vo
  • 5 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/PropFacts.vo
  • 5 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Inverse_Image.vo
  • 5 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Basics.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Control.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Eqdep.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Prelude.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Unicode/Utf8_core.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Relations.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/AltBinNotations.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NumPrelude.vo
  • 4 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Init.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Int.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrclasses.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Message.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssrmatching/ssrmatching.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/DecBool.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrsetoid.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Bool.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Utils.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Ltac2.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Inclusion.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellBasic.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Init.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Fresh.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Ltac1.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlBasic.vo
  • 3 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Option.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Ind.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Printf.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatClass.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/funind/FunInd.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/RelationalChoice.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Unicode/Utf8.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ExtensionalFunctionRepresentative.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Abstract/CarryType.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Env.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/String.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/AdmitAxiom.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Ident.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Char.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/Coq814.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/SetIsType.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/Coq815.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/Extraction.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/derive/Derive.vo
  • 2 K ../ocaml-base-compiler.4.10.2/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/Coq816.vo

Uninstall ๐Ÿงน

Command
opam remove -y coq-tactician-stdlib.dev
Return code
0
Missing removes
none
Wrong removes
none