« Up

tactician-stdlib 1.0~beta1+8.13 24 m 39 s

(2021-11-05 09:57:39 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              3           Virtual package relying on a GMP lib system installation
coq                   8.13.2      Formal proof management system
num                   1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                 4.12.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.12.0      Official release 4.12.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.1       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`. Then exactly the same `.vo`
  files are installed, except that they also contain Tactician's tactic databases.
  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"
]
post-messages: ["
--- The standard library was successfully recompiled ---
In order to finish the process, you should run
tactician recompile
" {success}]
depends: [
  "coq" {>= "8.13" & < "8.14~"}
  "coq-tactician"
]
build: [
  [make "-j%{jobs}%"]
]
install: [
  [make "install"]
]
remove: [
  [make "restore"]
]
url {
  src: "https://github.com/coq-tactician/coq-tactician-stdlib/archive/1.0-beta1-8.13.tar.gz"
}
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.1.0~beta1+8.13 coq.8.13.2
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.1.0~beta1+8.13 coq.8.13.2
Return code
0
Duration
6 m 13 s

Install

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-tactician-stdlib.1.0~beta1+8.13 coq.8.13.2
Return code
0
Duration
24 m 39 s

Installation size

Total: 52 M

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

Uninstall

Command
opam remove -y coq-tactician-stdlib.1.0~beta1+8.13
Return code
0
Missing removes
none
Wrong removes
none