# Packages matching: installed # Name # Installed # Synopsis base-bigarray base base-threads base base-unix base conf-findutils 1 Virtual package relying on findutils conf-gmp 4 Virtual package relying on a GMP lib system installation coq 8.13.0 Formal proof management system num 1.4 The legacy Num library for arbitrary-precision integer and rational arithmetic ocaml 4.09.1 The OCaml compiler (virtual package) ocaml-base-compiler 4.09.1 Official release 4.09.1 ocaml-config 1 OCaml Switch Configuration ocamlfind 1.9.5 A library manager for OCaml zarith 1.12 Implements arithmetic and logical operations over arbitrary-precision integers # opam file: opam-version: "2.0" 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" ]
true
Dry install with the current Coq version:
opam install -y --show-action coq-tactician-stdlib.1.0~beta1+8.13 coq.8.13.0
Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
true
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-tactician-stdlib.1.0~beta1+8.13 coq.8.13.0
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-tactician-stdlib.1.0~beta1+8.13 coq.8.13.0
Total: 52 M
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapAVL.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapFullAVL.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersEx.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetRBT.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetAVL.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/BinInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetAVL.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Hexadecimal.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Field_theory.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/Byte.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/BinNat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/List.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZBits.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZProperties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/PeanoNat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int31/Cyclic31.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapWeakList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NBits.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_polynom.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/BinPos.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetProperties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NProperties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetProperties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Tauto.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrbool.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetGenTree.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RiemannInt_SF.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RiemannInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/Int63.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZLcm.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ratan.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetInterface.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/Ascii.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZLog.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Binary/ZBinary.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/EnvRing.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZDivEucl.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetEqProperties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/RingMicromega.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZDivTrunc.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetEqProperties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZMicromega.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZDivFloor.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Peano/NPeano.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Binary/NBinary.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZSqrt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetPositive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NLcm.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Decimal.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetCompat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RIneq.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring_polynom.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/POrderedType.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapPositive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Alembert.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ClassicalDedekindReals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZGcd.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NDefOps.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetPositive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis5.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZPow.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/SetoidList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NLog.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NGcd.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalPos.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveRcomplete.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/NatPairs/ZNatPairs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/GenericMinMax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NPow.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NDiv.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/QArith_base.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Permutation.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtopology.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetDecide.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetDecide.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/btauto/Algebra.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZParity.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Byte.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/InitialRing.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NSqrt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NParity.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveReals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZPow.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_theory.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZAxioms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZDiv.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/NewtonInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Specif.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZMulOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetWeakList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetToFiniteSet.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NSub.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveRealsMorphisms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetBridge.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZMaxMin.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ChoiceFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSetFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/ZModulo/ZModulo.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalQ.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NIso.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetToFiniteSet.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NStrongRec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveCauchyReals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis_reg.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalQ.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NMaxMin.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZGcd.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveCauchyAbs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatLemmas.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZAddOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring_initial.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalNat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZParity.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrderedTypeEx.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Znumtheory.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalPos.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NAxioms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Cring.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/omega/PreOmega.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZMulOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Logic.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NMulOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/OrderedRing.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/EquivDec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZAdd.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalR.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZLt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalR.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NAddOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetWeakList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveMinMax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rfunctions.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/nsatz/NsatzTactic.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rpower.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SeqProp.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/PSeries_reg.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrderedType.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZMul.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Exp_prop.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Runcountable.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Znat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/PermutSetoid.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/VectorSpec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cos_plus.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zdiv.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NAdd.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ncring_tac.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/QExtra.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/Vector.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndigits.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/CMorphisms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/Orders.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Natural/Abstract/NBase.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveSum.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Int.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrfun.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSetInterface.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zquot.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/RList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalNat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZDomain.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyInst.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/RMicromega.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rdefinitions.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveLUB.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qcanon.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Bool.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZAxioms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveLimits.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/MVT.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Integer/Abstract/ZBase.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Lexicographic_Product.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rderiv.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Morphisms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Field_tac.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/rtauto/Bintree.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rlimit.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/PartSum.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rsqrt_def.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rprod.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/String.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/VectorDef.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis3.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/R_Ifp.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMapInterface.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cos_rel.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/Cyclic63.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rbasic_fun.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/RelationClasses.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/SpecFloat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/CPermutation.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_def.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rminmax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZAddOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Notations.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/EqualitiesFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ClassicalConstructiveReals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zgcd_alt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Raxioms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int31/Int31.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/SetoidDec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_reg.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersTac.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/BinPosDef.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Datatypes.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/R_sqrt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_alt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/CRelationClasses.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_calc.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/rtauto/Rtauto.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qpower.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/FinFun.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/BinIntDef.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zorder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rseries.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/btauto/Reflect.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Heap.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Machin.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SeqSeries.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis4.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/HexString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/AltSeries.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy_prod.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/Equalities.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/Fin.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalZ.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/ListSet.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssreflect.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_tac.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructiveAbs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpower.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Hurkens.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpow_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zeuclid.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qminmax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Even.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/omega/OmegaLemmas.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Sqrt_reg.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/PermutEq.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qreals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/WKL.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zdigits.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Abstract/ConstructivePower.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/QMicromega.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/DecidableTypeEx.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rgeom.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZCoeff.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rsigma.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Binomial.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Lexicographic_Exponentiation.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersLists.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/R_sqr.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Equality.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/EqdepFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/nsatz/Nsatz.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyInt63.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ROrderedType.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/SetoidPermutation.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/Pnat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Relation_Operators.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Rings_R.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ConstructiveEpsilon.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndist.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zeven.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalZ.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/BinNatDef.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZProperties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qabs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrdersAlt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/RealField.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/ArithProp.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qreduction.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/OctalString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Integral_domain.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZBits.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Mergesort.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/ZArith_dec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyComparison.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int31/Ring31.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyBool.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyClasses.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rcomplete.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rlogic.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Nat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/OrderedTypeAlt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/RelationPairs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/CEquivalence.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Sorted.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo_fun.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qround.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/FunctionalExtensionality.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/QOrderedType.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Structures/DecidableType.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zbool.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Diaconescu.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Powerset_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Tactics.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Between.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/HexadecimalN.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/PrimFloat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Nnat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Int63/Ring63.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Powerset_Classical_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qcabs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qfield.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Finite_sets_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/DecidableClass.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatAxioms.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlNativeString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/DecimalN.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Ltac.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Cpo.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/BinaryString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Reals.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Ranalysis.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zwf.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlChar.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Integration.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rtrigo.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Array/PArray.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Strings/ByteVector.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Psatz.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Equivalence.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Compare_dec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Lra.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Ztac.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/DiscrR.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Fourier_util.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zcomplements.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Tactics.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOCamlFloats.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Wf_nat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Wf_Z.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Multiset.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Infinite_sets.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatOps.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZMul.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Rings_Q.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/ConstructiveExtra.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/SetoidClass.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Refl.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zcompare.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZArith_hints.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Eqdep_dec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlIntConv.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlBigIntConv.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Morphisms_Prop.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Image.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/MExtraction.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/Floats.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NaryFunctions.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Operators_Properties.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Peano.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Cauchy/PosExtra.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rregisternames.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Fourier.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZAdd.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SplitAbsolu.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalEpsilon.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Vectors/VectorEq.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlZInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/SplitRmult.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Plus.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlZBigInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FSets.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rpow_def.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Reals/Rbase.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Ensembles.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Env.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/MSets/MSets.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Lqa.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOCamlInt63.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Rings_Z.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/DeclConstant.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Lia.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Euclid.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Div2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Number.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/Streams.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/FSets/FMaps.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/ArithRing.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zhints.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/auxiliary.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Mult.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOCamlPArray.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellZInteger.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellZInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/WeakFan.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellZNum.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalDescription.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/VarMap.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/ListDec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/btauto/Btauto.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Epsilon.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/ZArithRing.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zabs.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/ZArith.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Wf.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/omega/Omega.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpow_alt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Morphisms_Relations.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/SetoidTactics.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Decidable.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Uniset.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Integers.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Bvector.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Gt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalChoice.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Lt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Classical_Prop.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/SetoidChoice.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/EqNat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/NArithRing.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/ZArith_base.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/StreamMemo.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/BinList.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Zerob.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Classical_sets.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Powerset.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlNatInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlNatBigInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/IndefiniteDescription.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellNatNum.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zmin.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/QArith.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/Zify.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zmax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ExtensionalityFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/BoolOrder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/Cyclic/Abstract/DoubleType.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/NArith.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/omega/OmegaTactic.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/omega/OmegaPlugin.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/QArith/Qring.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Peano_dec.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Minus.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Wf.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Lists/ListTactics.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/funind/Recdef.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Description.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Field.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Max.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/List.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Relation_Definitions.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/JMeq.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlString.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellNatInteger.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellNatInt.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/micromega/ZifyPow.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Ring_base.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zmisc.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zpow_def.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Arith.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Bool_nat.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Berardi.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Min.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/HLevels.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NatInt/NZBase.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Constructive_sets.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Tauto.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ZArith/Zminmax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ClassicalUniqueChoice.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_3_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Compare.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Le.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Std.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_2_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Partial_Order.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Classical_Pred_Type.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Program.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/setoid_ring/Algebra_syntax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Subset.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ndiv_def.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Factorial.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Syntax.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sorting/Sorting.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Wellfounded.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Notations.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Well_Ordering.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Arith/Arith_base.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/PropExtensionality.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Ngcd_def.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Finite_sets.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Classical.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Array.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/NArith/Nsqrt_def.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_1_facts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/Sumbool.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/PArith/PArith.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Combinators.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Setoids/Setoid.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/StrictProp.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/BinNums.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Relations_3.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/BoolEq.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ProofIrrelevanceFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/PropExtensionalityFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Disjoint_Union.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/IfProp.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Sets/Permut.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrunder.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Union.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Logic_Type.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ProofIrrelevance.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Transitive_Closure.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Basics.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Inverse_Image.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/Eqdep.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Pattern.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/PropFacts.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Prelude.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Unicode/Utf8_core.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Relations/Relations.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/AltBinNotations.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Control.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Constr.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Classes/Init.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrclasses.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Numbers/NumPrelude.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Bool/DecBool.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssrmatching/ssrmatching.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Program/Utils.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrHaskellBasic.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssr/ssrsetoid.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Wellfounded/Inclusion.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/ExtrOcamlBasic.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Ltac2.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Init.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Fresh.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Option.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Int.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Floats/FloatClass.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Init/Numeral.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/funind/FunInd.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/RelationalChoice.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Ltac1.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/ExtensionalFunctionRepresentative.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Unicode/Utf8.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Message.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Bool.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Env.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/ssrsearch/ssrsearch.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/String.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Ident.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/AdmitAxiom.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/Coq812.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/user-contrib/Ltac2/Char.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/Coq811.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Logic/SetIsType.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/extraction/Extraction.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/derive/Derive.vo
../ocaml-base-compiler.4.09.1/lib/coq/user-contrib/tactician-stdlib-backup/theories/Compat/Coq813.vo
opam remove -y coq-tactician-stdlib.1.0~beta1+8.13