Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/c/coq-ext-lib/coq-ext-lib_0.11.6-2_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/coq-ext-lib-0.11.6-2ekuxbm4c/coq-ext-lib_0.11.6-2_amd64.buildinfo Get source package info: coq-ext-lib=0.11.6-2 Source URL: http://snapshot.notset.fr/mr/package/coq-ext-lib/0.11.6-2/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.71-2 automake=1:1.16.5-1.3 autopoint=0.21-6 autotools-dev=20220109.1 base-files=12.2 base-passwd=3.5.52 bash=5.1-6.1 binutils=2.38.50.20220707-1 binutils-common=2.38.50.20220707-1 binutils-x86-64-linux-gnu=2.38.50.20220707-1 bsdextrautils=2.38-5 bsdutils=1:2.38-4 build-essential=12.9 bzip2=1.0.8-5 coq=8.15.2+dfsg-2 coreutils=8.32-4.1 cpp=4:11.2.0-2 cpp-11=11.3.0-4 dash=0.5.11+git20210903+057cd650a4ed-8 debconf=1.5.79 debhelper=13.8 debianutils=5.7-0.2 dh-autoreconf=20 dh-coq=0.3 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.13.0-1 diffutils=1:3.7-5 dpkg=1.21.9 dpkg-dev=1.21.9 dwz=0.14-1 file=1:5.41-4 findutils=4.9.0-3 g++=4:11.2.0-2 g++-11=11.3.0-4 gcc=4:11.2.0-2 gcc-11=11.3.0-4 gcc-11-base=11.3.0-4 gcc-12-base=12.1.0-5 gettext=0.21-6 gettext-base=0.21-6 grep=3.7-1 groff-base=1.22.4-8 gzip=1.12-1 hostname=3.23 init-system-helpers=1.64 intltool-debian=0.35.0+20060710.5 libacl1=2.3.1-1 libarchive-zip-perl=1.68-1 libasan6=11.3.0-4 libatomic1=12.1.0-5 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libbinutils=2.38.50.20220707-1 libblkid1=2.38-4 libbz2-1.0=1.0.8-5 libc-bin=2.33-8 libc-dev-bin=2.33-8 libc6=2.33-8 libc6-dev=2.33-8 libcap-ng0=0.8.3-1 libcap2=1:2.44-1 libcc1-0=12.1.0-5 libcom-err2=1.46.5-2 libcoq-core-ocaml=8.15.2+dfsg-2 libcoq-core-ocaml-dev=8.15.2+dfsg-2 libcoq-stdlib=8.15.2+dfsg-2 libcrypt-dev=1:4.4.28-2 libcrypt1=1:4.4.28-2 libctf-nobfd0=2.38.50.20220707-1 libctf0=2.38.50.20220707-1 libdb5.3=5.3.28+dfsg1-0.10 libdebconfclient0=0.263 libdebhelper-perl=13.8 libdpkg-perl=1.21.9 libelf1=0.187-1 libexpat1=2.4.8-1 libffi8=3.4.2-4 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libgcc-11-dev=11.3.0-4 libgcc-s1=12.1.0-5 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libgmp-dev=2:6.2.1+dfsg1-1 libgmp10=2:6.2.1+dfsg1-1 libgmp3-dev=2:6.2.1+dfsg1-1 libgmpxx4ldbl=2:6.2.1+dfsg1-1 libgomp1=12.1.0-5 libgpg-error0=1.45-2 libgprofng0=2.38.50.20220707-1 libgssapi-krb5-2=1.19.2-2+b2 libicu71=71.1-3 libisl23=0.24-2 libitm1=12.1.0-5 libk5crypto3=1.19.2-2+b2 libkeyutils1=1.6.3-1 libkrb5-3=1.19.2-2+b2 libkrb5support0=1.19.2-2+b2 liblsan0=12.1.0-5 liblz4-1=1.9.3-2 liblzma5=5.2.5-2.1 libmagic-mgc=1:5.41-4 libmagic1=1:5.41-4 libmount1=2.38-4 libmpc3=1.2.1-2 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libncurses-dev=6.3+20220423-2 libncurses5-dev=6.3+20220423-2 libncurses6=6.3+20220423-2 libncursesw6=6.3+20220423-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libpam-modules=1.4.0-13 libpam-modules-bin=1.4.0-13 libpam-runtime=1.4.0-13 libpam0g=1.4.0-13 libpcre2-8-0=10.40-1 libpcre3=2:8.39-14 libperl5.34=5.34.0-5 libpipeline1=1.5.6-1 libpython3-stdlib=3.10.4-1+b1 libpython3.10-minimal=3.10.5-1 libpython3.10-stdlib=3.10.5-1 libquadmath0=12.1.0-5 libreadline8=8.1.2-1.2 libseccomp2=2.5.4-1 libselinux1=3.4-1 libsigsegv2=2.14-1 libsmartcols1=2.38-4 libsqlite3-0=3.39.1-1 libssl3=3.0.4-2 libstdc++-11-dev=11.3.0-4 libstdc++6=12.1.0-5 libsub-override-perl=0.09-3 libsystemd0=251.2-8 libtinfo6=6.3+20220423-2 libtirpc-common=1.3.2-2 libtirpc-dev=1.3.2-2 libtirpc3=1.3.2-2 libtool=2.4.7-4 libtsan0=11.3.0-4 libubsan1=12.1.0-5 libuchardet0=0.0.7-1 libudev1=251.2-8 libunistring2=1.0-1 libuuid1=2.38-4 libxml2=2.9.14+dfsg-1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.5.2+dfsg-1 linux-libc-dev=5.18.5-1 login=1:4.11.1+dfsg1-2 lsb-base=11.2 m4=1.4.18-5 make=4.3-4.1 man-db=2.10.2-1 mawk=1.3.4.20200120-3.1 media-types=8.0.0 ncurses-base=6.3+20220423-2 ncurses-bin=6.3+20220423-2 ocaml=4.13.1-3 ocaml-base=4.13.1-3 ocaml-compiler-libs=4.13.1-3 ocaml-findlib=1.9.3-1 ocaml-interp=4.13.1-3 ocaml-nox=4.13.1-3 patch=2.7.6-7 perl=5.34.0-5 perl-base=5.34.0-5 perl-modules-5.34=5.34.0-5 po-debconf=1.0.21+nmu1 python3=3.10.4-1+b1 python3-minimal=3.10.4-1+b1 python3.10=3.10.5-1 python3.10-minimal=3.10.5-1 readline-common=8.1.2-1.2 rpcsvc-proto=1.4.2-4 sed=4.8-1 sensible-utils=0.0.17 sysvinit-utils=3.03-1 tar=1.34+dfsg-1 util-linux=2.38-4 util-linux-extra=2.38-4 xz-utils=5.2.5-2.1 zlib1g=1:1.2.11.dfsg-4 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220718T031307Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220718T031307Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220722T150935Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220713T220842Z/ unstable main' >> /etc/apt/sources.list && apt-get update" --customize-hook=chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash --customize-hook=chroot "$1" env sh -c "apt-get source --only-source -d coq-ext-lib=0.11.6-2 && mkdir -p /build/coq-ext-lib-pnyvJb && dpkg-source --no-check -x /*.dsc /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6 && chown -R builduser:builduser /build/coq-ext-lib-pnyvJb" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1657967831" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/coq-ext-lib-pnyvJb /tmp/coq-ext-lib-0.11.6-2ekuxbm4c bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220713T220842Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: null I: using /tmp/mmdebstrap.M8Zx1M2z0Y as tempdir I: running apt-get update... I: downloading packages with apt... I: extracting archives... I: installing essential packages... I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "apt-get --yes install fakeroot util-linux"' exec /tmp/mmdebstrap.M8Zx1M2z0Y Reading package lists... Building dependency tree... util-linux is already the newest version (2.38-4). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 136 kB of archives. After this operation, 401 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20220713T220842Z unstable/main amd64 libfakeroot amd64 1.29-1 [48.5 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220713T220842Z unstable/main amd64 fakeroot amd64 1.29-1 [87.3 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 136 kB in 0s (1084 kB/s) Selecting previously unselected package libfakeroot:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 4623 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.29-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.29-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.29-1_amd64.deb ... Unpacking fakeroot (1.29-1) ... Setting up libfakeroot:amd64 (1.29-1) ... Setting up fakeroot (1.29-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.33-8) ... I: running special hook: copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220718T031307Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220718T031307Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220722T150935Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220713T220842Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.M8Zx1M2z0Y Get:1 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm InRelease [130 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220722T150935Z unstable InRelease [192 kB] Hit:3 http://snapshot.notset.fr/archive/debian/20220713T220842Z unstable InRelease Ign:4 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main amd64 Packages Get:4 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main Sources [12.1 MB] Get:5 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main amd64 Packages [11.5 MB] Ign:6 http://snapshot.notset.fr/archive/debian/20220722T150935Z unstable/main amd64 Packages Err:6 http://snapshot.notset.fr/archive/debian/20220722T150935Z unstable/main amd64 Packages 404 Not Found [IP: 10.13.0.253 80] Ign:6 http://snapshot.notset.fr/archive/debian/20220722T150935Z unstable/main amd64 Packages Get:6 http://snapshot.notset.fr/archive/debian/20220722T150935Z unstable/main amd64 Packages [12.6 MB] Fetched 36.5 MB in 29s (1255 kB/s) Reading package lists... I: installing remaining packages inside the chroot... I: running --customize-hook in shell: sh -c 'chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash' exec /tmp/mmdebstrap.M8Zx1M2z0Y I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d coq-ext-lib=0.11.6-2 && mkdir -p /build/coq-ext-lib-pnyvJb && dpkg-source --no-check -x /*.dsc /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6 && chown -R builduser:builduser /build/coq-ext-lib-pnyvJb"' exec /tmp/mmdebstrap.M8Zx1M2z0Y Reading package lists... NOTICE: 'coq-ext-lib' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/coq-ext-lib.git Please use: git clone https://salsa.debian.org/ocaml-team/coq-ext-lib.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 86.6 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main coq-ext-lib 0.11.6-2 (dsc) [2084 B] Get:2 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main coq-ext-lib 0.11.6-2 (tar) [82.6 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220718T031307Z bookworm/main coq-ext-lib 0.11.6-2 (diff) [1956 B] Fetched 86.6 kB in 0s (890 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'coq-ext-lib_0.11.6-2.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting coq-ext-lib in /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6 dpkg-source: info: unpacking coq-ext-lib_0.11.6.orig.tar.gz dpkg-source: info: unpacking coq-ext-lib_0.11.6-2.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6 && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1657967831" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.M8Zx1M2z0Y dpkg-buildpackage: info: source package coq-ext-lib dpkg-buildpackage: info: source version 0.11.6-2 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Julien Puydt dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with coq debian/rules override_dh_auto_clean make[1]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' # not good make[1]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' dh_clean debian/rules binary-arch dh binary-arch --with coq dh_update_autotools_config -a dh_autoreconf -a dh_auto_configure -a dh_auto_build -a make -j10 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq make[2]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' COQDEP VFILES COQC theories/Core/RelDec.v COQC theories/Tactics/Injection.v COQC theories/Tactics/Forward.v COQC theories/Core/Any.v COQC theories/Core/EquivDec.v COQC theories/Core/Decision.v COQC theories/Structures/BinOps.v COQC theories/Structures/CoMonad.v COQC theories/Data/PreFun.v COQC theories/Data/Checked.v File "./theories/Core/Any.v", line 13, characters 0-66: Warning: The default value for hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated] COQC theories/Data/Eq/UIP_trans.v COQC theories/Data/ListNth.v COQC theories/Data/LazyList.v COQC theories/Data/ListFirstnSkipn.v COQC theories/Data/N.v COQC theories/Data/Prop.v COQC theories/Data/Stream.v COQC theories/Programming/Injection.v COQC theories/Programming/With.v COQC theories/Recur/Facts.v COQC theories/Recur/GenRec.v COQC theories/Recur/Measure.v COQC theories/Relations/TransitiveClosure.v COQC theories/Relations/Compose.v COQC theories/Tactics/BoolTac.v COQC theories/Tactics/Parametric.v File "./theories/Tactics/BoolTac.v", line 6, characters 0-66: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] COQC theories/Tactics/Reify.v COQC theories/Data/Graph/Graph.v COQC theories/Tactics/Hide.v File "./theories/Programming/With.v", line 59, characters 0-39: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope struct_scope.". [undeclared-scope,deprecated] COQC theories/ExtLib.v COQC theories/Tactics/Consider.v COQC theories/Structures/Functor.v COQC theories/Structures/CoFunctor.v File "./theories/Programming/Injection.v", line 12, characters 0-86: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] File "./theories/Tactics/Consider.v", line 104, characters 0-128: Warning: The default value for hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated] File "./theories/Programming/Injection.v", line 15, characters 0-99: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] File "./theories/Programming/Injection.v", line 17, characters 0-100: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] COQC theories/Structures/CoMonadLaws.v COQC theories/Structures/Monoid.v COQC theories/Data/Unit.v COQC theories/Data/Bool.v COQC theories/Data/Eq.v COQC theories/Data/Pair.v COQC theories/Data/Positive.v COQC theories/Data/Sum.v COQC theories/Data/Z.v File "./theories/Data/Eq.v", line 31, characters 0-37: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] File "./theories/Data/Eq.v", line 43, characters 0-38: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] COQC theories/Data/PPair.v File "./theories/Data/Eq.v", line 76, characters 0-33: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] COQC theories/Programming/Eqv.v File "./theories/Data/Eq.v", line 91, characters 0-31: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] File "./theories/Data/Eq.v", line 96, characters 0-35: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] COQC theories/Programming/Le.v COQC theories/Recur/Relation.v File "./theories/Programming/Le.v", line 11, characters 0-126: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] File "./theories/Programming/Le.v", line 14, characters 0-109: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] COQC theories/Tactics/Equality.v File "./theories/Programming/Le.v", line 32, characters 0-108: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] COQC theories/Tactics/Cases.v COQC theories/Structures/EqDep.v COQC theories/Core/CmpDec.v File "./theories/Data/ListFirstnSkipn.v", line 48, characters 0-91: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] File "./theories/Programming/Eqv.v", line 12, characters 0-114: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] File "./theories/Data/ListFirstnSkipn.v", line 93, characters 0-86: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] COQC theories/Structures/Applicative.v COQC theories/Structures/Foldable.v COQC theories/Structures/Sets.v COQC theories/Data/Char.v COQC theories/Data/Nat.v COQC theories/Tactics/EqDep.v COQC theories/Data/Fun.v COQC theories/Structures/Monad.v COQC theories/Structures/Traversable.v COQC theories/Data/POption.v COQC theories/Structures/FunctorLaws.v COQC theories/Tactics.v COQC theories/Data/Fin.v COQC theories/Data/SigT.v File "./theories/Structures/Monad.v", line 56, characters 2-39: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope monad_scope.". [undeclared-scope,deprecated] File "./theories/Data/POption.v", line 83, characters 0-34: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] File "./theories/Data/POption.v", line 88, characters 0-38: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] COQC theories/Data/PList.v COQC theories/Structures/Reducible.v COQC theories/Structures/MonadCont.v COQC theories/Structures/MonadExc.v COQC theories/Structures/MonadFix.v COQC theories/Structures/MonadZero.v COQC theories/Structures/MonadPlus.v COQC theories/Structures/MonadReader.v COQC theories/Structures/MonadWriter.v File "./theories/Data/SigT.v", line 42, characters 0-32: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] COQC theories/Structures/MonadState.v COQC theories/Structures/MonadTrans.v COQC theories/Data/Lazy.v COQC theories/Data/String.v COQC theories/Data/Monads/IdentityMonad.v COQC theories/Data/Monads/ContMonad.v COQC theories/Structures/Maps.v COQC theories/Data/Option.v COQC theories/Data/Tuple.v COQC theories/Data/Vector.v COQC theories/Structures/Monads.v COQC theories/Data/Set/SetMap.v COQC theories/Structures/MonadLaws.v COQC theories/Data/List.v File "./theories/Data/PList.v", line 219, characters 0-32: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] COQC theories/Programming/Extras.v COQC theories/Data/Monads/StateMonad.v COQC theories/Data/Monads/WriterMonad.v COQC theories/Data/Monads/FuelMonad.v COQC theories/Data/Monads/OptionMonad.v COQC theories/Data/Map/FMapTwoThreeK.v File "./theories/Data/Option.v", line 183, characters 0-34: Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding rewriting hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Rewrite foo : bar." [deprecated-hint-rewrite-without-locality,deprecated] COQC theories/Data/Monads/EitherMonad.v COQC theories/Data/Monads/ReaderMonad.v COQC theories/Data/Member.v COQC theories/Data/Map/FMapPositive.v COQC theories/Tactics/MonadTac.v COQC theories/Data/Monads/FuelMonadLaws.v COQC theories/Data/Monads/IdentityMonadLaws.v COQC theories/Data/Monads/OptionMonadLaws.v COQC theories/Data/Monads/ReaderMonadLaws.v COQC theories/Data/Set/TwoThreeTrees.v COQC theories/Data/Graph/BuildGraph.v COQC theories/Data/Graph/GraphAlgos.v COQC theories/Data/Map/FMapAList.v COQC theories/Data/Set/ListSet.v COQC theories/Data/HList.v COQC theories/Generic/Func.v COQC theories/Data/Graph/GraphAdjList.v COQC theories/Programming/Show.v File "./theories/Programming/Show.v", line 64, characters 2-37: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope show_scope.". [undeclared-scope,deprecated] COQC theories/Generic/Ind.v File "./theories/Generic/Ind.v", line 135, characters 0-72: Warning: The default value for hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated] File "./theories/Generic/Ind.v", line 136, characters 0-72: Warning: The default value for hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding hints outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated] = "-(5,-(6,-(7,-())))" : string COQC theories/Data/SumN.v COQC theories/Generic/Data.v COQC theories/Generic/DerivingData.v make[2]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' make -C examples make[2]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/examples' coq_makefile -f _CoqProject -o Makefile.coq Warning: ../theories (used in -R or -Q) is not a subdirectory of the current directory Warning: No common logical root. Warning: In this case the -docroot option should be given. Warning: Otherwise the install-doc target is going to install files Warning: in orphan_ExtLib_ExtLibExamples make -f Makefile.coq make[3]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/examples' COQDEP VFILES COQC ConsiderDemo.v COQC EvalWithExc.v COQC MonadReasoning.v COQC Printing.v COQC UsingSets.v COQC WithDemo.v COQC Notations.v COQC StateTMonad.v File "./StateTMonad.v", line 11, characters 0-31: Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time being, adding instances outside of sections without specifying an explicit locality attribute is therefore deprecated. It is recommended to use "export" whenever possible. Use the attributes #[local], #[global] and #[export] depending on your choice. For example: "#[export] Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated] = {| a := true; b := 1; c := false |} : RTest = RTest -> false = false : Prop = (tt, ?ST 1 (string -> string) String {| Monoid.monoid_plus := fun (g f : string -> string) (x : string) => g (f x); Monoid.monoid_unit := fun x : string => x |} (?ST0@{u:=tt} 2 (string -> string) String {| Monoid.monoid_plus := fun (g f : string -> string) (x : string) => g (f x); Monoid.monoid_unit := fun x : string => x |} ""%string)) : unit * string = (tt, String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii false false true true false true false false) (String (Ascii.Ascii false false false false false true false false) (String (Ascii.Ascii true true true false false true false false) (String (Ascii.Ascii true false true false false true true false) (String (...) (...)))))))))))))))))))))))) : unit * string = (tt, String (Ascii.Ascii false false false true false true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii false false true true false true true false) (String (Ascii.Ascii true true true true false true true false) (String (Ascii.Ascii false false false false false true false false) (?ST@{u:=tt} 2 (string -> string) String {| Monoid.monoid_plus := fun (g f : string -> string) (x : string) => g (f x); Monoid.monoid_unit := fun x : string => x |} ""%string))))))) : unit * string = inr (Int 3) : string + value = inl "expected integer got bool"%string : string + value = false : bool = ?Foldable_set (list ?V) cons nil ((let (_, _, _, _, _, _, _, _, add, _) := ?DSet in add) true ((let (_, _, _, _, _, _, _, _, add, _) := ?DSet0 in add) true (let (_, empty, _, _, _, _, _, _, _, _) := ?DSet1 in empty))) : list ?V = (let (fmap) := ?Functor in fmap) bool bool (fun b : bool => if b then false else true) ((let (_, _, _, _, _, _, _, _, add, _) := ?DSet in add) true (let (_, empty, _, _, _, _, _, _, _, _) := ?DSet0 in empty)) : ?F bool make[3]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/examples' make[2]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/examples' make[1]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' dh: command-omitted: The call to "dh_auto_test -a" was omitted due to "DEB_BUILD_OPTIONS=nocheck" create-stamp debian/debhelper-build-stamp dh_prep -a debian/rules override_dh_auto_install make[1]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' make install DESTDIR=/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp make[2]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' make -f Makefile.coq install make[3]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' INSTALL theories/ExtLib.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib/ INSTALL theories/Tactics.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib/ INSTALL theories/Core/Any.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/CmpDec.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/EquivDec.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/RelDec.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/Decision.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Structures/Applicative.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/BinOps.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoFunctor.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoMonadLaws.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/EqDep.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Foldable.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/FunctorLaws.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Functor.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Maps.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadCont.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadExc.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadFix.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadLaws.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadPlus.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadReader.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadState.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monads.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadTrans.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadWriter.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadZero.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monoid.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Reducible.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Sets.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Traversable.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Data/Bool.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Char.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Checked.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Eq.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Eq/UIP_trans.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Eq INSTALL theories/Data/Fin.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Fun.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/HList.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/LazyList.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Lazy.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/ListFirstnSkipn.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/ListNth.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/List.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Member.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Nat.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/N.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Option.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Pair.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Positive.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PreFun.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Prop.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/SigT.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Stream.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/String.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/SumN.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Sum.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Tuple.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Unit.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Vector.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Z.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/POption.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PList.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PPair.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Generic/Data.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/DerivingData.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/Func.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/Ind.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Programming/Eqv.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Extras.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Injection.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Le.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Show.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/With.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Recur/Facts.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/GenRec.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/Measure.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/Relation.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Relations/Compose.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Relations INSTALL theories/Relations/TransitiveClosure.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Relations INSTALL theories/Tactics/BoolTac.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Cases.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Consider.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/EqDep.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Equality.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Forward.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Injection.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/MonadTac.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Parametric.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Reify.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Hide.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Data/Graph/BuildGraph.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/GraphAdjList.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/GraphAlgos.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/Graph.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Map/FMapAList.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Map/FMapPositive.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Map/FMapTwoThreeK.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Monads/ContMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/EitherMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/FuelMonadLaws.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/FuelMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/IdentityMonadLaws.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/IdentityMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/OptionMonadLaws.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/OptionMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/ReaderMonadLaws.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/ReaderMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/StateMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/WriterMonad.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Set/ListSet.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/Data/Set/SetMap.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/Data/Set/TwoThreeTrees.vo /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/ExtLib.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib/ INSTALL theories/Tactics.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib/ INSTALL theories/Core/Any.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/CmpDec.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/EquivDec.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/RelDec.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/Decision.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Structures/Applicative.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/BinOps.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoFunctor.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoMonadLaws.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/EqDep.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Foldable.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/FunctorLaws.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Functor.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Maps.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadCont.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadExc.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadFix.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadLaws.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadPlus.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadReader.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadState.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monads.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadTrans.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadWriter.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadZero.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monoid.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Reducible.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Sets.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Traversable.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Data/Bool.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Char.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Checked.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Eq.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Eq/UIP_trans.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Eq INSTALL theories/Data/Fin.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Fun.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/HList.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/LazyList.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Lazy.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/ListFirstnSkipn.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/ListNth.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/List.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Member.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Nat.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/N.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Option.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Pair.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Positive.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PreFun.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Prop.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/SigT.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Stream.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/String.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/SumN.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Sum.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Tuple.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Unit.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Vector.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Z.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/POption.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PList.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PPair.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Generic/Data.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/DerivingData.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/Func.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/Ind.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Programming/Eqv.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Extras.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Injection.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Le.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Show.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/With.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Recur/Facts.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/GenRec.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/Measure.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/Relation.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Relations/Compose.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Relations INSTALL theories/Relations/TransitiveClosure.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Relations INSTALL theories/Tactics/BoolTac.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Cases.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Consider.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/EqDep.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Equality.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Forward.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Injection.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/MonadTac.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Parametric.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Reify.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Hide.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Data/Graph/BuildGraph.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/GraphAdjList.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/GraphAlgos.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/Graph.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Map/FMapAList.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Map/FMapPositive.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Map/FMapTwoThreeK.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Monads/ContMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/EitherMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/FuelMonadLaws.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/FuelMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/IdentityMonadLaws.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/IdentityMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/OptionMonadLaws.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/OptionMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/ReaderMonadLaws.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/ReaderMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/StateMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/WriterMonad.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Set/ListSet.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/Data/Set/SetMap.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/Data/Set/TwoThreeTrees.v /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/ExtLib.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib/ INSTALL theories/Tactics.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib/ INSTALL theories/Core/Any.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/CmpDec.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/EquivDec.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/RelDec.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Core/Decision.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Core INSTALL theories/Structures/Applicative.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/BinOps.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoFunctor.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/CoMonadLaws.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/EqDep.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Foldable.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/FunctorLaws.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Functor.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Maps.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadCont.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadExc.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadFix.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadLaws.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadPlus.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadReader.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadState.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monads.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadTrans.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadWriter.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/MonadZero.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Monoid.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Reducible.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Sets.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Structures/Traversable.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Structures INSTALL theories/Data/Bool.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Char.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Checked.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Eq.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Eq/UIP_trans.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Eq INSTALL theories/Data/Fin.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Fun.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/HList.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/LazyList.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Lazy.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/ListFirstnSkipn.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/ListNth.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/List.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Member.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Nat.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/N.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Option.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Pair.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Positive.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PreFun.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Prop.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/SigT.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Stream.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/String.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/SumN.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Sum.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Tuple.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Unit.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Vector.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/Z.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/POption.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PList.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Data/PPair.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data INSTALL theories/Generic/Data.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/DerivingData.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/Func.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Generic/Ind.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Generic INSTALL theories/Programming/Eqv.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Extras.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Injection.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Le.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/Show.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Programming/With.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Programming INSTALL theories/Recur/Facts.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/GenRec.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/Measure.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Recur/Relation.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Recur INSTALL theories/Relations/Compose.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Relations INSTALL theories/Relations/TransitiveClosure.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Relations INSTALL theories/Tactics/BoolTac.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Cases.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Consider.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/EqDep.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Equality.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Forward.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Injection.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/MonadTac.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Parametric.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Reify.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Tactics/Hide.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Tactics INSTALL theories/Data/Graph/BuildGraph.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/GraphAdjList.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/GraphAlgos.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Graph/Graph.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Graph INSTALL theories/Data/Map/FMapAList.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Map/FMapPositive.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Map/FMapTwoThreeK.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Map INSTALL theories/Data/Monads/ContMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/EitherMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/FuelMonadLaws.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/FuelMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/IdentityMonadLaws.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/IdentityMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/OptionMonadLaws.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/OptionMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/ReaderMonadLaws.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/ReaderMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/StateMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Monads/WriterMonad.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Monads INSTALL theories/Data/Set/ListSet.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/Data/Set/SetMap.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set INSTALL theories/Data/Set/TwoThreeTrees.glob /build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6/debian/tmp//usr/lib/ocaml/coq//user-contrib/ExtLib//Data/Set make[4]: Entering directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' make[4]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' make[3]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' make[2]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' make[1]: Leaving directory '/build/coq-ext-lib-pnyvJb/coq-ext-lib-0.11.6' dh_install -a dh_installdocs -a dh_installchangelogs -a dh_installexamples -a dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a dh_missing -a dh_dwz -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_coq -a dh_gencontrol -a dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libcoq-ext-lib' in '../libcoq-ext-lib_0.11.6-2_amd64.deb'. dpkg-genbuildinfo --build=any -O../coq-ext-lib_0.11.6-2_amd64.buildinfo dpkg-genchanges --build=any -O../coq-ext-lib_0.11.6-2_amd64.changes dpkg-genchanges: info: binary-only arch-specific upload (source code and arch-indep packages not included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: running special hook: sync-out /build/coq-ext-lib-pnyvJb /tmp/coq-ext-lib-0.11.6-2ekuxbm4c I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap.M8Zx1M2z0Y... I: success in 562.2317 seconds md5: Value of 'md5' differs for libcoq-ext-lib_0.11.6-2_amd64.deb sha1: Value of 'sha1' differs for libcoq-ext-lib_0.11.6-2_amd64.deb sha256: Value of 'sha256' differs for libcoq-ext-lib_0.11.6-2_amd64.deb Checksums: FAIL Cannot generate diffoscope for libcoq-ext-lib_0.11.6-2_amd64.deb: RetryError[]