Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/c/coq-deriving/coq-deriving_0.1.0-1+b1_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/coq-deriving-0.1.0-1+b14oa9v0ii/coq-deriving_0.1.0-1+b1_amd64.buildinfo Get source package info: coq-deriving=0.1.0-1 Source URL: http://snapshot.notset.fr/mr/package/coq-deriving/0.1.0-1/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.90.20220713-2 binutils-common=2.38.90.20220713-2 binutils-x86-64-linux-gnu=2.38.90.20220713-2 bsdextrautils=2.38-5 bsdutils=1:2.38-5 build-essential=12.9 bzip2=1.0.8-5 coq=8.15.2+dfsg-2 coreutils=8.32-4.1 cpp=4:12.1.0-3 cpp-12=12.1.0-7 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:12.1.0-3 g++-12=12.1.0-7 gcc=4:12.1.0-3 gcc-12=12.1.0-7 gcc-12-base=12.1.0-7 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 libasan8=12.1.0-7 libatomic1=12.1.0-7 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libbinutils=2.38.90.20220713-2 libblkid1=2.38-5 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+b1 libcap2=1:2.44-1 libcc1-0=12.1.0-7 libcom-err2=1.46.5-2 libcoq-core-ocaml=8.15.2+dfsg-2 libcoq-core-ocaml-dev=8.15.2+dfsg-2 libcoq-mathcomp-ssreflect=1.15.0-1 libcoq-stdlib=8.15.2+dfsg-2 libcrypt-dev=1:4.4.28-2 libcrypt1=1:4.4.28-2 libctf-nobfd0=2.38.90.20220713-2 libctf0=2.38.90.20220713-2 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-12-dev=12.1.0-7 libgcc-s1=12.1.0-7 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-7 libgpg-error0=1.45-2 libgprofng0=2.38.90.20220713-2 libgssapi-krb5-2=1.20-1 libicu71=71.1-3 libisl23=0.25-1 libitm1=12.1.0-7 libk5crypto3=1.20-1 libkeyutils1=1.6.3-1 libkrb5-3=1.20-1 libkrb5support0=1.20-1 liblsan0=12.1.0-7 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-5 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.5-3 libpython3.10-minimal=3.10.5-1 libpython3.10-stdlib=3.10.5-1 libquadmath0=12.1.0-7 libreadline8=8.1.2-1.2 libseccomp2=2.5.4-1+b1 libselinux1=3.4-1+b1 libsigsegv2=2.14-1 libsmartcols1=2.38-5 libsqlite3-0=3.39.2-1 libssl3=3.0.5-1 libstdc++-12-dev=12.1.0-7 libstdc++6=12.1.0-7 libsub-override-perl=0.09-3 libsystemd0=251.3-1 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 libtsan2=12.1.0-7 libubsan1=12.1.0-7 libuchardet0=0.0.7-1 libudev1=251.3-1 libunistring2=1.0-1 libuuid1=2.38-5 libxml2=2.9.14+dfsg-1+b1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.5.2+dfsg-1 linux-libc-dev=5.18.14-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.5-3 python3-minimal=3.10.5-3 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-5 util-linux-extra=2.38-5 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/20220727T154516Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220728T094517Z/ 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-deriving=0.1.0-1 && mkdir -p /build/coq-deriving-LEq1rH && dpkg-source --no-check -x /*.dsc /build/coq-deriving-LEq1rH/coq-deriving-0.1.0 && cd /build/coq-deriving-LEq1rH/coq-deriving-0.1.0 && { printf '%s' 'coq-deriving (0.1.0-1+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuild on buildd -- amd64 / i386 Build Daemon (x86-ubc-01) Wed, 27 Jul 2022 00:40:06 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-deriving-LEq1rH" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-deriving-LEq1rH/coq-deriving-0.1.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658882406" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/coq-deriving-LEq1rH /tmp/coq-deriving-0.1.0-1+b14oa9v0ii bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220728T094517Z 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.iMCP0qaZOr 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.iMCP0qaZOr Reading package lists... Building dependency tree... util-linux is already the newest version (2.38-5). 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/20220728T094517Z unstable/main amd64 libfakeroot amd64 1.29-1 [48.5 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220728T094517Z 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 (994 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 ... 4629 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/20220727T154516Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220728T094517Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.iMCP0qaZOr Get:1 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm InRelease [157 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20220728T094517Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources [12.1 MB] Get:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages [11.5 MB] Fetched 23.8 MB in 22s (1059 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.iMCP0qaZOr I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d coq-deriving=0.1.0-1 && mkdir -p /build/coq-deriving-LEq1rH && dpkg-source --no-check -x /*.dsc /build/coq-deriving-LEq1rH/coq-deriving-0.1.0 && cd /build/coq-deriving-LEq1rH/coq-deriving-0.1.0 && { printf '%s' 'coq-deriving (0.1.0-1+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuild on buildd -- amd64 / i386 Build Daemon (x86-ubc-01) Wed, 27 Jul 2022 00:40:06 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-deriving-LEq1rH"' exec /tmp/mmdebstrap.iMCP0qaZOr Reading package lists... NOTICE: 'coq-deriving' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/coq-deriving.git Please use: git clone https://salsa.debian.org/ocaml-team/coq-deriving.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 33.3 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-deriving 0.1.0-1 (dsc) [2108 B] Get:2 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-deriving 0.1.0-1 (tar) [29.3 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-deriving 0.1.0-1 (diff) [1908 B] Fetched 33.3 kB in 0s (501 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'coq-deriving_0.1.0-1.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting coq-deriving in /build/coq-deriving-LEq1rH/coq-deriving-0.1.0 dpkg-source: info: unpacking coq-deriving_0.1.0.orig.tar.gz dpkg-source: info: unpacking coq-deriving_0.1.0-1.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-deriving-LEq1rH/coq-deriving-0.1.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658882406" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.iMCP0qaZOr dpkg-buildpackage: info: source package coq-deriving dpkg-buildpackage: info: source version 0.1.0-1+b1 dpkg-buildpackage: info: source distribution sid dpkg-buildpackage: info: source changed by amd64 / i386 Build Daemon (x86-ubc-01) dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with coq,ocaml debian/rules override_dh_auto_clean make[1]: Entering directory '/build/coq-deriving-LEq1rH/coq-deriving-0.1.0' Doesn't work as expected make[1]: Leaving directory '/build/coq-deriving-LEq1rH/coq-deriving-0.1.0' dh_ocamlclean dh_clean debian/rules binary-arch dh binary-arch --with coq,ocaml dh_update_autotools_config -a dh_autoreconf -a dh_ocamlinit -a dh_auto_configure -a dh_auto_build -a make -j10 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/coq-deriving-LEq1rH/coq-deriving-0.1.0' coq_makefile -f _CoqProject -o CoqMakefile make --no-print-directory -f CoqMakefile ocaml str.cma make_tactics.ml theories/ind.v theories/base.v > theories/tactics.v COQDEP TESTVFILES COQDEP VFILES COQC theories/base.v File "./theories/base.v", line 32, characters 0-28: 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/base.v", line 86, characters 0-36: 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/base.v", line 87, characters 0-38: 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/base.v", line 88, characters 0-30: 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/base.v", line 89, characters 0-28: 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/base.v", line 90, characters 0-30: 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/base.v", line 91, characters 0-31: 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/base.v", line 92, characters 0-27: 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/base.v", line 93, characters 0-27: 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/base.v", line 104, characters 0-26: 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/base.v", line 105, characters 0-26: 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/base.v", line 174, characters 0-37: 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/base.v", line 175, characters 0-38: 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/base.v", line 176, characters 0-44: 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/base.v", line 177, characters 0-44: 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/base.v", line 178, characters 0-37: 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/base.v", line 179, characters 0-36: 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/base.v", line 180, characters 0-38: 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/base.v", line 181, characters 0-37: 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/base.v", line 182, characters 0-36: 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/base.v", line 183, characters 0-40: 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/base.v", line 184, characters 0-36: 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/base.v", line 188, characters 0-27: 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/base.v", line 195, characters 0-31: 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/base.v", line 209, characters 0-32: 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/base.v", line 216, characters 0-31: 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/base.v", line 221, characters 0-28: 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/base.v", line 225, characters 0-29: 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/base.v", line 229, characters 0-28: 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/base.v", line 246, characters 0-31: 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/base.v", line 263, characters 0-33: 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/base.v", line 270, characters 0-34: 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/base.v", line 285, characters 0-28: 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/base.v", line 303, characters 0-34: 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/base.v", line 332, characters 0-32: 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/base.v", line 358, characters 0-34: 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/base.v", line 370, characters 0-35: 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/base.v", line 378, characters 0-35: 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/base.v", line 386, characters 0-34: 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/base.v", line 421, characters 0-34: 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/base.v", line 435, characters 0-35: 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/base.v", line 440, characters 0-34: 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/base.v", line 533, characters 0-29: 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/base.v", line 534, characters 0-28: 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/base.v", line 535, characters 0-36: 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/base.v", line 536, characters 0-35: 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/base.v", line 537, characters 0-36: 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/base.v", line 538, characters 0-36: 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/base.v", line 545, characters 0-28: 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/base.v", line 619, characters 0-28: 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/base.v", line 620, characters 0-29: 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/base.v", line 621, characters 0-27: 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/base.v", line 622, characters 0-29: 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/base.v", line 623, characters 0-29: 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/base.v", line 831, characters 0-29: 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/base.v", line 832, characters 0-30: 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/base.v", line 833, characters 0-30: 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/base.v", line 834, characters 0-28: 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/base.v", line 835, characters 0-29: 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/base.v", line 836, characters 0-28: 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/base.v", line 837, characters 0-30: 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/base.v", line 838, characters 0-29: 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/base.v", line 839, characters 0-29: 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/base.v", line 840, characters 0-31: 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/base.v", line 841, characters 0-29: 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/base.v", line 842, characters 0-29: 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/base.v", line 843, characters 0-28: 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/base.v", line 844, characters 0-36: 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/base.v", line 845, characters 0-36: 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/base.v", line 846, characters 0-36: 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/base.v", line 847, characters 0-33: 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/base.v", line 848, characters 0-34: 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/base.v", line 849, characters 0-29: 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/base.v", line 857, characters 0-28: 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/base.v", line 862, characters 0-29: 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/base.v", line 867, characters 0-29: 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/base.v", line 930, characters 0-28: 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/base.v", line 939, characters 0-32: 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/base.v", line 964, characters 0-31: 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/base.v", line 1121, characters 0-31: 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/base.v", line 1130, characters 0-30: 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/base.v", line 1137, characters 0-30: 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/base.v", line 1145, characters 0-29: 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/ind.v File "./theories/ind.v", line 30, characters 0-30: 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/ind.v", line 31, characters 0-28: 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/ind.v", line 32, characters 0-28: 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/ind.v", line 33, characters 0-34: 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/ind.v", line 78, characters 0-32: 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/ind.v", line 79, characters 0-34: 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/ind.v", line 80, characters 0-34: 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/ind.v", line 81, characters 0-35: 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/ind.v", line 82, characters 0-39: 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/ind.v", line 83, characters 0-40: 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/ind.v", line 84, characters 0-38: 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/ind.v", line 85, characters 0-39: 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/ind.v", line 86, characters 0-39: 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/ind.v", line 268, characters 0-35: 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/ind.v", line 269, characters 0-39: 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/ind.v", line 270, characters 0-30: 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/ind.v", line 271, characters 0-29: 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/ind.v", line 272, characters 0-33: 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/ind.v", line 273, characters 0-35: 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/ind.v", line 274, characters 0-34: 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/ind.v", line 275, characters 0-33: 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/ind.v", line 276, characters 0-37: 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/ind.v", line 277, characters 0-33: 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/ind.v", line 278, characters 0-37: 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/ind.v", line 279, characters 0-38: 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/ind.v", line 280, characters 0-35: 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/ind.v", line 281, characters 0-39: 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/ind.v", line 282, characters 0-40: 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/ind.v", line 283, characters 0-33: 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/ind.v", line 284, characters 0-37: 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/ind.v", line 285, characters 0-38: 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/ind.v", line 286, characters 0-34: 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/ind.v", line 287, characters 0-38: 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/ind.v", line 288, characters 0-39: 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/ind.v", line 289, characters 0-39: 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/ind.v", line 290, characters 0-36: 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/ind.v", line 291, characters 0-40: 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/ind.v", line 292, characters 0-38: 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/ind.v", line 293, characters 0-39: 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/ind.v", line 294, characters 0-36: 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/ind.v", line 295, characters 0-37: 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/ind.v", line 296, characters 0-36: 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/ind.v", line 297, characters 0-37: 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/ind.v", line 298, characters 0-37: 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/ind.v", line 299, characters 0-38: 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/ind.v", line 300, characters 0-33: 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/ind.v", line 313, characters 0-37: 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/ind.v", line 529, characters 0-139: 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/ind.v", line 534, characters 0-140: 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/ind.v", line 546, characters 0-32: 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/ind.v", line 547, characters 0-32: 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/ind.v", line 548, characters 0-36: 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/ind.v", line 549, characters 0-40: 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/ind.v", line 550, characters 0-38: 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/ind.v", line 551, characters 0-36: 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/ind.v", line 552, characters 0-39: 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/ind.v", line 553, characters 0-38: 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/ind.v", line 554, characters 0-36: 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/ind.v", line 555, characters 0-48: 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/ind.v", line 556, characters 0-48: 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/ind.v", line 557, characters 0-39: 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/ind.v", line 558, characters 0-38: 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/ind.v", line 559, characters 0-38: 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/ind.v", line 560, characters 0-41: 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/ind.v", line 561, characters 0-45: 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/ind.v", line 562, characters 0-50: 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/ind.v", line 563, characters 0-39: 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/ind.v", line 564, characters 0-38: 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/ind.v", line 565, characters 0-37: 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/ind.v", line 566, characters 0-36: 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/ind.v", line 567, characters 0-35: 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/ind.v", line 568, characters 0-36: 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/ind.v", line 569, characters 0-33: 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/ind.v", line 570, characters 0-37: 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/ind.v", line 571, characters 0-36: 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/ind.v", line 572, characters 0-37: 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/ind.v", line 573, characters 0-33: 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/ind.v", line 574, characters 0-31: 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/ind.v", line 575, characters 0-31: 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/ind.v", line 576, characters 0-32: 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/ind.v", line 577, characters 0-32: 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/ind.v", line 578, characters 0-33: 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/ind.v", line 579, characters 0-37: 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/ind.v", line 580, characters 0-38: 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/ind.v", line 581, characters 0-36: 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/ind.v", line 778, characters 0-35: 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/ind.v", line 779, characters 0-33: 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/ind.v", line 780, characters 0-33: 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/ind.v", line 781, characters 0-33: 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/ind.v", line 782, characters 0-48: 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/ind.v", line 783, characters 0-32: 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/ind.v", line 784, characters 0-38: 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/ind.v", line 785, characters 0-39: 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/ind.v", line 786, characters 0-41: 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/ind.v", line 787, characters 0-48: 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/ind.v", line 788, characters 0-33: 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/ind.v", line 789, characters 0-35: 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/ind.v", line 893, characters 0-39: 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/ind.v", line 894, characters 0-39: 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/ind.v", line 895, characters 0-42: 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/ind.v", line 896, characters 0-38: 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/ind.v", line 897, characters 0-39: 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/ind.v", line 898, characters 0-38: 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/ind.v", line 899, characters 0-38: 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/ind.v", line 900, characters 0-36: 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/ind.v", line 913, characters 0-79: 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/ind.v", line 924, characters 0-75: 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/ind.v", line 934, characters 0-77: 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/ind.v", line 962, characters 0-35: 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/ind.v", line 963, characters 0-39: 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/ind.v", line 964, characters 0-38: 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/ind.v", line 965, characters 0-42: 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/ind.v", line 966, characters 0-43: 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/ind.v", line 967, characters 0-40: 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/ind.v", line 968, characters 0-40: 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/ind.v", line 998, characters 0-39: 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/ind.v", line 999, characters 0-43: 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/ind.v", line 1000, characters 0-42: 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/ind.v", line 1001, characters 0-50: 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/ind.v", line 1002, characters 0-47: 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/ind.v", line 1003, characters 0-44: 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/ind.v", line 1004, characters 0-48: 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/ind.v", line 1005, characters 0-44: 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/ind.v", line 1037, characters 0-38: 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/ind.v", line 1038, characters 0-42: 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/ind.v", line 1039, characters 0-41: 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/ind.v", line 1040, characters 0-48: 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/ind.v", line 1041, characters 0-46: 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/ind.v", line 1042, characters 0-43: 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/ind.v", line 1043, characters 0-47: 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/ind.v", line 1044, characters 0-46: 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/ind.v", line 1045, characters 0-43: 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/tactics.v COQC theories/infer.v File "./theories/infer.v", line 49, characters 0-439: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 49, characters 0-439: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 49, characters 0-439: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 49, characters 0-439: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 58, characters 0-379: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 58, characters 0-379: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 58, characters 0-379: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 58, characters 0-379: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] File "./theories/infer.v", line 58, characters 0-379: Warning: grammar entry "ident" permitted "_" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use "name" instead. [deprecated-ident-entry,deprecated] COQC theories/instances/eqtype.v COQC theories/instances/tree_of_ind.v COQC theories/instances/fintype.v COQC theories/instances/order.v COQC theories/instances.v COQC theories/deriving.v make[1]: Leaving directory '/build/coq-deriving-LEq1rH/coq-deriving-0.1.0' 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-deriving-LEq1rH/coq-deriving-0.1.0' DESTDIR=debian/tmp make install make[2]: Entering directory '/build/coq-deriving-LEq1rH/coq-deriving-0.1.0' coq_makefile -f _CoqProject -o CoqMakefile make --no-print-directory -f CoqMakefile install INSTALL theories/base.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/ind.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/tactics.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/infer.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/instances.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/deriving.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/instances/eqtype.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/tree_of_ind.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/fintype.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/order.vo debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/base.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/ind.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/tactics.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/infer.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/instances.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/deriving.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/instances/eqtype.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/tree_of_ind.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/fintype.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/order.v debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/base.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/ind.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/tactics.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/infer.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/instances.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/deriving.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving/ INSTALL theories/instances/eqtype.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/tree_of_ind.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/fintype.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances INSTALL theories/instances/order.glob debian/tmp//usr/lib/ocaml/coq//user-contrib/deriving//instances make[2]: Leaving directory '/build/coq-deriving-LEq1rH/coq-deriving-0.1.0' make[1]: Leaving directory '/build/coq-deriving-LEq1rH/coq-deriving-0.1.0' dh_install -a dh_ocamldoc -a dh_installdocs -a dh_installchangelogs -a dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a dh_missing -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_coq -a dh_ocaml -a dh_gencontrol -a dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libcoq-deriving' in '../libcoq-deriving_0.1.0-1+b1_amd64.deb'. dpkg-genbuildinfo --build=any -O../coq-deriving_0.1.0-1+b1_amd64.buildinfo dpkg-genchanges --build=any -O../coq-deriving_0.1.0-1+b1_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-deriving-LEq1rH /tmp/coq-deriving-0.1.0-1+b14oa9v0ii I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap.iMCP0qaZOr... I: success in 934.1174 seconds md5: Value of 'md5' differs for libcoq-deriving_0.1.0-1+b1_amd64.deb md5: Size differs for libcoq-deriving_0.1.0-1+b1_amd64.deb sha1: Value of 'sha1' differs for libcoq-deriving_0.1.0-1+b1_amd64.deb sha1: Size differs for libcoq-deriving_0.1.0-1+b1_amd64.deb sha256: Value of 'sha256' differs for libcoq-deriving_0.1.0-1+b1_amd64.deb sha256: Size differs for libcoq-deriving_0.1.0-1+b1_amd64.deb Checksums: FAIL Cannot generate diffoscope for libcoq-deriving_0.1.0-1+b1_amd64.deb: RetryError[]