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