Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/c/coq-bignums/coq-bignums_8.15.0-2_amd64.buildinfo
Use metasnap for getting required timestamps
New buildinfo file: /tmp/coq-bignums-8.15.0-29ph5a1ge/coq-bignums_8.15.0-2_amd64.buildinfo
Get source package info: coq-bignums=8.15.0-2
Source URL: http://snapshot.notset.fr/mr/package/coq-bignums/8.15.0-2/srcfiles?fileinfo=1
env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.71-2 automake=1:1.16.5-1.3 autopoint=0.21-6 autotools-dev=20220109.1 base-files=12.2 base-passwd=3.5.52 bash=5.1-6+b1 binutils=2.38-4 binutils-common=2.38-4 binutils-x86-64-linux-gnu=2.38-4 bsdextrautils=2.38-4 bsdutils=1:2.38-4 build-essential=12.9 bzip2=1.0.8-5 coq=8.15.1+dfsg-2 coreutils=8.32-4.1 cpp=4:11.2.0-2 cpp-11=11.3.0-1 dash=0.5.11+git20210903+057cd650a4ed-8 debconf=1.5.79 debhelper=13.7.1 debianutils=5.7-0.2 dh-autoreconf=20 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.13.0-1 diffutils=1:3.7-5 dpkg=1.21.7 dpkg-dev=1.21.7 dwz=0.14-1 file=1:5.41-4 findutils=4.9.0-3 g++=4:11.2.0-2 g++-11=11.3.0-1 gcc=4:11.2.0-2 gcc-11=11.3.0-1 gcc-11-base=11.3.0-1 gcc-12-base=12.1.0-2 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.62 intltool-debian=0.35.0+20060710.5 libacl1=2.3.1-1 libarchive-zip-perl=1.68-1 libasan6=11.3.0-1 libatomic1=12.1.0-2 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libbinutils=2.38-4 libblkid1=2.38-4 libbz2-1.0=1.0.8-5 libc-bin=2.33-7 libc-dev-bin=2.33-7 libc6=2.33-7 libc6-dev=2.33-7 libcap-ng0=0.7.9-2.2+b2 libcap2=1:2.44-1 libcc1-0=12.1.0-2 libcom-err2=1.46.5-2 libcoq-core-ocaml=8.15.1+dfsg-2 libcoq-core-ocaml-dev=8.15.1+dfsg-2 libcoq-stdlib=8.15.1+dfsg-2 libcrypt-dev=1:4.4.27-1.1 libcrypt1=1:4.4.27-1.1 libctf-nobfd0=2.38-4 libctf0=2.38-4 libdb5.3=5.3.28+dfsg1-0.9 libdebconfclient0=0.262 libdebhelper-perl=13.7.1 libdpkg-perl=1.21.7 libelf1=0.187-1 libexpat1=2.4.8-1 libffi8=3.4.2-4 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libgcc-11-dev=11.3.0-1 libgcc-s1=12.1.0-2 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libgmp-dev=2:6.2.1+dfsg-3 libgmp10=2:6.2.1+dfsg-3 libgmp3-dev=2:6.2.1+dfsg-3 libgmpxx4ldbl=2:6.2.1+dfsg-3 libgomp1=12.1.0-2 libgpg-error0=1.45-2 libgssapi-krb5-2=1.19.2-2+b2 libicu71=71.1-3 libisl23=0.24-2 libitm1=12.1.0-2 libk5crypto3=1.19.2-2+b2 libkeyutils1=1.6.1-3 libkrb5-3=1.19.2-2+b2 libkrb5support0=1.19.2-2+b2 liblsan0=12.1.0-2 liblz4-1=1.9.3-2 liblzma5=5.2.5-2.1 libmagic-mgc=1:5.41-4 libmagic1=1:5.41-4 libmount1=2.38-4 libmpc3=1.2.1-2 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libncurses-dev=6.3+20220423-2 libncurses5-dev=6.3+20220423-2 libncurses6=6.3+20220423-2 libncursesw6=6.3+20220423-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libpam-modules=1.4.0-13 libpam-modules-bin=1.4.0-13 libpam-runtime=1.4.0-13 libpam0g=1.4.0-13 libpcre2-8-0=10.40-1 libpcre3=2:8.39-14 libperl5.34=5.34.0-4 libpipeline1=1.5.6-1 libpython3-stdlib=3.10.4-1+b1 libpython3.10-minimal=3.10.4-4+b1 libpython3.10-stdlib=3.10.4-4+b1 libquadmath0=12.1.0-2 libreadline8=8.1.2-1.2 libseccomp2=2.5.4-1 libselinux1=3.3-1+b2 libsigsegv2=2.14-1 libsmartcols1=2.38-4 libsqlite3-0=3.38.5-1 libssl3=3.0.3-4 libstdc++-11-dev=11.3.0-1 libstdc++6=12.1.0-2 libsub-override-perl=0.09-2 libsystemd0=250.4-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 libtsan0=11.3.0-1 libubsan1=12.1.0-2 libuchardet0=0.0.7-1 libudev1=250.4-1 libunistring2=1.0-1 libuuid1=2.38-4 libxml2=2.9.14+dfsg-1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.5.2+dfsg-1 linux-libc-dev=5.17.6-1+b1 login=1:4.11.1+dfsg1-2 lsb-base=11.1.0 m4=1.4.18-5 make=4.3-4.1 man-db=2.10.2-1 mawk=1.3.4.20200120-3+b1 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-4 perl-base=5.34.0-4 perl-modules-5.34=5.34.0-4 po-debconf=1.0.21+nmu1 python3=3.10.4-1+b1 python3-minimal=3.10.4-1+b1 python3.10=3.10.4-4+b1 python3.10-minimal=3.10.4-4+b1 readline-common=8.1.2-1.2 rpcsvc-proto=1.4.2-4 sed=4.8-1 sensible-utils=0.0.17 sysvinit-utils=3.03-1 tar=1.34+dfsg-1 util-linux=2.38-4 util-linux-extra=2.38-4 xz-utils=5.2.5-2.1 zlib1g=1:1.2.11.dfsg-4 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220522T213641Z/ unstable main
deb-src http://snapshot.notset.fr/archive/debian/20220522T213641Z/ unstable main
deb http://snapshot.notset.fr/archive/debian/20220531T213137Z/ unstable main
deb http://snapshot.notset.fr/archive/debian/20220519T145256Z/ 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-bignums=8.15.0-2 && mkdir -p /build/coq-bignums-E6lzsD && dpkg-source --no-check -x /*.dsc /build/coq-bignums-E6lzsD/coq-bignums-8.15.0 && chown -R builduser:builduser /build/coq-bignums-E6lzsD" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-bignums-E6lzsD/coq-bignums-8.15.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1653240285" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/coq-bignums-E6lzsD /tmp/coq-bignums-8.15.0-29ph5a1ge bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220519T145256Z 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.ijWsCT1IAO 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.ijWsCT1IAO
Reading package lists...
Building dependency tree...
util-linux is already the newest version (2.38-4).
The following NEW packages will be installed:
  fakeroot libfakeroot
0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded.
Need to get 135 kB of archives.
After this operation, 406 kB of additional disk space will be used.
Get:1 http://snapshot.notset.fr/archive/debian/20220519T145256Z unstable/main amd64 libfakeroot amd64 1.28-1 [48.2 kB]
Get:2 http://snapshot.notset.fr/archive/debian/20220519T145256Z unstable/main amd64 fakeroot amd64 1.28-1 [87.2 kB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 135 kB in 0s (975 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.28-1_amd64.deb ...
Unpacking libfakeroot:amd64 (1.28-1) ...
Selecting previously unselected package fakeroot.
Preparing to unpack .../fakeroot_1.28-1_amd64.deb ...
Unpacking fakeroot (1.28-1) ...
Setting up libfakeroot:amd64 (1.28-1) ...
Setting up fakeroot (1.28-1) ...
update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode
Processing triggers for libc-bin (2.33-7) ...
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/20220522T213641Z/ unstable main
deb-src http://snapshot.notset.fr/archive/debian/20220522T213641Z/ unstable main
deb http://snapshot.notset.fr/archive/debian/20220531T213137Z/ unstable main
deb http://snapshot.notset.fr/archive/debian/20220519T145256Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.ijWsCT1IAO
Get:1 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable InRelease [165 kB]
Get:2 http://snapshot.notset.fr/archive/debian/20220531T213137Z unstable InRelease [165 kB]
Hit:3 http://snapshot.notset.fr/archive/debian/20220519T145256Z unstable InRelease
Ign:4 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main Sources
Ign:5 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main amd64 Packages
Ign:4 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main Sources
Ign:5 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main amd64 Packages
Ign:4 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main Sources
Ign:5 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main amd64 Packages
Get:4 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main Sources [12.9 MB]
Get:5 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main amd64 Packages [12.4 MB]
Ign:6 http://snapshot.notset.fr/archive/debian/20220531T213137Z unstable/main amd64 Packages
Err:6 http://snapshot.notset.fr/archive/debian/20220531T213137Z unstable/main amd64 Packages
  404  Not Found [IP: 10.13.0.253 80]
Ign:6 http://snapshot.notset.fr/archive/debian/20220531T213137Z unstable/main amd64 Packages
Get:6 http://snapshot.notset.fr/archive/debian/20220531T213137Z unstable/main amd64 Packages [12.5 MB]
Fetched 38.1 MB in 31s (1218 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.ijWsCT1IAO
I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d coq-bignums=8.15.0-2 && mkdir -p /build/coq-bignums-E6lzsD && dpkg-source --no-check -x /*.dsc /build/coq-bignums-E6lzsD/coq-bignums-8.15.0 && chown -R builduser:builduser /build/coq-bignums-E6lzsD"' exec /tmp/mmdebstrap.ijWsCT1IAO
Reading package lists...
NOTICE: 'coq-bignums' packaging is maintained in the 'Git' version control system at:
https://salsa.debian.org/ocaml-team/coq-bignums.git
Please use:
git clone https://salsa.debian.org/ocaml-team/coq-bignums.git
to retrieve the latest (possibly unreleased) updates to the package.
Need to get 119 kB of source archives.
Get:1 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main coq-bignums 8.15.0-2 (dsc) [2188 B]
Get:2 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main coq-bignums 8.15.0-2 (tar) [115 kB]
Get:3 http://snapshot.notset.fr/archive/debian/20220522T213641Z unstable/main coq-bignums 8.15.0-2 (diff) [1796 B]
Fetched 119 kB in 0s (571 kB/s)
Download complete and in download only mode
W: Download is performed unsandboxed as root as file 'coq-bignums_8.15.0-2.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied)
dpkg-source: info: extracting coq-bignums in /build/coq-bignums-E6lzsD/coq-bignums-8.15.0
dpkg-source: info: unpacking coq-bignums_8.15.0.orig.tar.gz
dpkg-source: info: unpacking coq-bignums_8.15.0-2.debian.tar.xz
I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-bignums-E6lzsD/coq-bignums-8.15.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1653240285" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.ijWsCT1IAO
dpkg-buildpackage: info: source package coq-bignums
dpkg-buildpackage: info: source version 8.15.0-2
dpkg-buildpackage: info: source distribution unstable
dpkg-buildpackage: info: source changed by Julien Puydt <jpuydt@debian.org>
 dpkg-source --before-build .
dpkg-buildpackage: info: host architecture amd64
 debian/rules clean
dh clean --with ocaml
   dh_auto_clean
	make -j10 clean
make[1]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make -f Makefile.coq Makefile
make[2]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make[2]: Nothing to be done for 'Makefile'.
make[2]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make -f Makefile.coq clean
make[2]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
rm -f BigN/NMake_gen.v
CLEAN
make[2]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
rm -f Makefile.coq Makefile.coq.conf
make[1]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
   dh_ocamlclean
   dh_clean
 debian/rules binary-arch
dh binary-arch --with ocaml
   dh_update_autotools_config -a
   dh_autoreconf -a
   dh_ocamlinit -a
   dh_auto_configure -a
   debian/rules override_dh_auto_build
make[1]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make
make[2]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq Makefile
make[3]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
ocaml BigN/gen/NMake_gen.ml > BigN/NMake_gen.v || (RV=$?; rm -f BigN/NMake_gen.v; exit ${RV})
COQDEP VFILES
OCAMLLIBDEP plugin/bignums_syntax_plugin.mlpack
CAMLDEP plugin/bignums_syntax.ml
make[3]: Nothing to be done for 'Makefile'.
make[3]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make -f Makefile.coq all
make[3]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
CAMLOPT -c -for-pack Bignums_syntax_plugin plugin/bignums_syntax.ml
CAMLOPT -pack -o plugin/bignums_syntax_plugin.cmx
CAMLOPT -a -o plugin/bignums_syntax_plugin.cmxa
CAMLOPT -shared -o plugin/bignums_syntax_plugin.cmxs
COQC BigNumPrelude.v
File "./BigNumPrelude.v", line 52, characters 0-242:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./BigNumPrelude.v", line 52, characters 0-242:
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 "./BigNumPrelude.v", line 59, characters 0-227:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./BigNumPrelude.v", line 59, characters 0-227:
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 "./BigNumPrelude.v", line 67, 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 "./BigNumPrelude.v", line 127, characters 0-89:
Warning: The default value for rewriting hint locality is currently "local"
in a section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding rewriting hints outside of sections
without specifying an explicit locality attribute is therefore deprecated. It
is recommended to use "export" whenever possible. Use the attributes
#[local], #[global] and #[export] depending on your choice. For example:
"#[export] Hint Rewrite foo : bar."
[deprecated-hint-rewrite-without-locality,deprecated]
COQC CyclicDouble/DoubleBase.v
COQC CyclicDouble/DoubleAdd.v
COQC CyclicDouble/DoubleSub.v
COQC CyclicDouble/DoubleMul.v
COQC CyclicDouble/DoubleSqrt.v
File "./CyclicDouble/DoubleSqrt.v", line 676, characters 1-23:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
COQC CyclicDouble/DoubleLift.v
COQC CyclicDouble/DoubleDivn1.v
COQC CyclicDouble/DoubleDiv.v
COQC CyclicDouble/DoubleCyclic.v
File "./CyclicDouble/DoubleCyclic.v", line 825, characters 1-26:
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
File "./CyclicDouble/DoubleCyclic.v", line 958, characters 1-41:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./CyclicDouble/DoubleCyclic.v", line 959, characters 1-49:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC BigN/Nbasic.v
File "./BigN/Nbasic.v", line 296, characters 8-9:
Warning: Unused variable r catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/Nbasic.v", line 354, characters 8-9:
Warning: Unused variable r catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
File "./BigN/Nbasic.v", line 505, characters 0-46:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/Nbasic.v", line 506, characters 0-51:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC SpecViaZ/NSig.v
COQC BigN/NMake_gen.v
File "./BigN/NMake_gen.v", line 38, characters 1-50:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 39, characters 1-50:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 40, characters 1-50:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 41, characters 1-60:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 42, characters 1-60:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 43, characters 1-60:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 44, characters 1-69:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 45, characters 1-69:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 46, characters 1-69:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 72, characters 1-87:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 125, characters 1-44:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 249, characters 1-38:
Warning: The default value for Typeclasses Opaque and Typeclasses Transparent
locality is currently "local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time being, adding typeclass
transparency 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] Typeclasses Transparent
foo." [deprecated-typeclasses-transparency-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 251, characters 1-47:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 252, characters 1-60:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 253, characters 1-60:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 254, characters 1-60:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 255, characters 1-70:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 256, characters 1-70:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 257, characters 1-70:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 258, characters 1-70:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 260, characters 1-50:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 267, characters 1-49:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigN/NMake_gen.v", line 272, characters 1-179:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 593, characters 1-68:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 603, characters 1-76:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 611, characters 1-119:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
File "./BigN/NMake_gen.v", line 619, characters 1-119:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
COQC BigN/NMake.v
File "./BigN/NMake.v", line 250, characters 1-141:
Warning: Interpreting this declaration as if a global declaration prefixed by
"Local", i.e. as a global declaration which shall not be available without
qualification when imported. [local-declaration,scope]
COQC SpecViaZ/NSigNAxioms.v
File "./SpecViaZ/NSigNAxioms.v", line 15, characters 0-365:
Warning: The default value for rewriting hint locality is currently "local"
in a section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding rewriting hints outside of sections
without specifying an explicit locality attribute is therefore deprecated. It
is recommended to use "export" whenever possible. Use the attributes
#[local], #[global] and #[export] depending on your choice. For example:
"#[export] Hint Rewrite foo : bar."
[deprecated-hint-rewrite-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 29, characters 0-35:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 32, characters 0-49:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 33, characters 0-49:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 34, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 35, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 36, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 167, characters 0-62:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 172, characters 0-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 177, characters 0-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 182, characters 0-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 187, characters 0-47:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 226, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 316, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 317, characters 0-55:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 367, characters 0-66:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/NSigNAxioms.v", line 450, characters 0-119:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC BigN/BigN.v
File "./BigN/BigN.v", line 130, characters 8-18:
Warning: Tactic isInt63cst is deprecated since 8.14. Use isUint63cst instead
[deprecated-tactic,deprecated]
COQC SpecViaZ/ZSig.v
COQC SpecViaZ/ZSigZAxioms.v
File "./SpecViaZ/ZSigZAxioms.v", line 15, characters 0-388:
Warning: The default value for rewriting hint locality is currently "local"
in a section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding rewriting hints outside of sections
without specifying an explicit locality attribute is therefore deprecated. It
is recommended to use "export" whenever possible. Use the attributes
#[local], #[global] and #[export] depending on your choice. For example:
"#[export] Hint Rewrite foo : bar."
[deprecated-hint-rewrite-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 28, characters 0-35:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 33, characters 0-51:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 34, characters 0-51:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 35, characters 0-56:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 36, characters 0-56:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 37, characters 0-56:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 178, characters 0-62:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 183, characters 0-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 188, characters 0-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 193, characters 0-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 198, characters 0-47:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 237, characters 0-49:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 278, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 362, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 363, characters 0-55:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 388, characters 0-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 389, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaZ/ZSigZAxioms.v", line 446, characters 0-66:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC SpecViaQ/QSig.v
File "./SpecViaQ/QSig.v", line 99, characters 0-155:
Warning: The default value for rewriting hint locality is currently "local"
in a section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding rewriting hints outside of sections
without specifying an explicit locality attribute is therefore deprecated. It
is recommended to use "export" whenever possible. Use the attributes
#[local], #[global] and #[export] depending on your choice. For example:
"#[export] Hint Rewrite foo : bar."
[deprecated-hint-rewrite-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 117, characters 0-30:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 118, characters 0-35:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 123, characters 0-51:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 124, characters 0-51:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 125, characters 0-47:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 126, characters 0-66:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 127, characters 0-66:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 128, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 129, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 130, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 131, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 132, characters 0-47:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 133, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 134, characters 0-53:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 135, characters 0-47:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 136, characters 0-52:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 137, characters 0-62:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./SpecViaQ/QSig.v", line 147, characters 0-38:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC BigQ/QMake.v
File "./BigQ/QMake.v", line 87, characters 1-329:
Warning: The default value for rewriting hint locality is currently "local"
in a section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding rewriting hints outside of sections
without specifying an explicit locality attribute is therefore deprecated. It
is recommended to use "export" whenever possible. Use the attributes
#[local], #[global] and #[export] depending on your choice. For example:
"#[export] Hint Rewrite foo : bar."
[deprecated-hint-rewrite-without-locality,deprecated]
File "./BigQ/QMake.v", line 349, characters 1-87:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 382, characters 1-64:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 405, characters 1-86:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 562, characters 1-107:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 647, characters 1-94:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 827, characters 1-69:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 898, characters 1-87:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 961, characters 1-75:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 1014, characters 1-80:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./BigQ/QMake.v", line 1042, characters 1-54:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC BigZ/ZMake.v
COQC BigZ/BigZ.v
COQC BigQ/BigQ.v
make[3]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make[2]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make[1]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.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-bignums-E6lzsD/coq-bignums-8.15.0'
dh_auto_install
	make -j10 install DESTDIR=/build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true"
make[2]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make -f Makefile.coq Makefile
make[3]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make[3]: Nothing to be done for 'Makefile'.
make[3]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make -f Makefile.coq install
make[3]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
INSTALL BigN/Nbasic.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/NMake.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/BigN.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums/
INSTALL BigZ/ZMake.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.vo /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigZ
INSTALL BigN/Nbasic.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/NMake.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/BigN.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums/
INSTALL BigZ/ZMake.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.v /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigZ
INSTALL BigN/Nbasic.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/NMake.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/NMake_gen.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL BigN/BigN.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigN
INSTALL SpecViaZ/NSig.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSig.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/NSigNAxioms.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaZ/ZSigZAxioms.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaZ
INSTALL SpecViaQ/QSig.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//SpecViaQ
INSTALL BigQ/QMake.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigQ
INSTALL BigQ/BigQ.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigQ
INSTALL CyclicDouble/DoubleBase.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleAdd.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDiv.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleMul.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSub.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleDivn1.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleSqrt.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleCyclic.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL CyclicDouble/DoubleLift.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//CyclicDouble
INSTALL BigNumPrelude.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums/
INSTALL BigZ/ZMake.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigZ
INSTALL BigZ/BigZ.glob /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//BigZ
INSTALL plugin/bignums_syntax_plugin.cmi /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxs /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxs /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmxa /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//plugin
INSTALL plugin/bignums_syntax_plugin.cmx /build/coq-bignums-E6lzsD/coq-bignums-8.15.0/debian/tmp//usr/lib/ocaml/coq//user-contrib/Bignums//plugin
make[4]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make[4]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make[3]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
make[2]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
find debian/tmp -regextype posix-awk \
  -regex '.*\.(v|vo|vos|glob)$' \
          >> debian/libcoq-bignums.install
find debian/tmp -regextype posix-awk \
  -regex '.*\.(a|cmi|cmo|cmt|cmti|cmx|cmxa|ml|mli|o)$' \
          >> debian/libcoq-bignums-ocaml-dev.install
make[1]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
   dh_install -a
   dh_ocamldoc -a
   dh_installdocs -a
   dh_installchangelogs -a
   dh_lintian -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_ocaml -a
   debian/rules override_dh_gencontrol
make[1]: Entering directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
dh_gencontrol -- -VF:CoqABI="8.15.1+4.13.1"
dpkg-gencontrol: warning: Provides field of package libcoq-bignums: substitution variable ${ocaml:Provides} used, but is not defined
dpkg-gencontrol: warning: package libcoq-bignums-ocaml-dev: substitution variable ${ocaml:Depends} unused, but is defined
dpkg-gencontrol: warning: package libcoq-bignums-ocaml: substitution variable ${ocaml:Depends} unused, but is defined
dpkg-gencontrol: warning: package libcoq-bignums-ocaml: substitution variable ${ocaml:Depends} unused, but is defined
make[1]: Leaving directory '/build/coq-bignums-E6lzsD/coq-bignums-8.15.0'
   dh_md5sums -a
   dh_builddeb -a
dpkg-deb: building package 'libcoq-bignums' in '../libcoq-bignums_8.15.0-2_amd64.deb'.
dpkg-deb: building package 'libcoq-bignums-ocaml' in '../libcoq-bignums-ocaml_8.15.0-2_amd64.deb'.
dpkg-deb: building package 'libcoq-bignums-ocaml-dbgsym' in '../libcoq-bignums-ocaml-dbgsym_8.15.0-2_amd64.deb'.
dpkg-deb: building package 'libcoq-bignums-ocaml-dev' in '../libcoq-bignums-ocaml-dev_8.15.0-2_amd64.deb'.
 dpkg-genbuildinfo --build=any -O../coq-bignums_8.15.0-2_amd64.buildinfo
 dpkg-genchanges --build=any -O../coq-bignums_8.15.0-2_amd64.changes
dpkg-genchanges: info: binary-only arch-specific upload (source code and arch-indep packages not included)
 dpkg-source --after-build .
dpkg-buildpackage: info: binary-only upload (no source included)
I: running special hook: sync-out /build/coq-bignums-E6lzsD /tmp/coq-bignums-8.15.0-29ph5a1ge
I: cleaning package lists and apt cache...
I: removing tempdir /tmp/mmdebstrap.ijWsCT1IAO...
I: success in 827.3056 seconds
md5: libcoq-bignums-ocaml-dbgsym_8.15.0-2_amd64.deb: OK
md5: libcoq-bignums-ocaml-dev_8.15.0-2_amd64.deb: OK
md5: libcoq-bignums-ocaml_8.15.0-2_amd64.deb: OK
md5: libcoq-bignums_8.15.0-2_amd64.deb: OK
sha1: libcoq-bignums-ocaml-dbgsym_8.15.0-2_amd64.deb: OK
sha1: libcoq-bignums-ocaml-dev_8.15.0-2_amd64.deb: OK
sha1: libcoq-bignums-ocaml_8.15.0-2_amd64.deb: OK
sha1: libcoq-bignums_8.15.0-2_amd64.deb: OK
sha256: libcoq-bignums-ocaml-dbgsym_8.15.0-2_amd64.deb: OK
sha256: libcoq-bignums-ocaml-dev_8.15.0-2_amd64.deb: OK
sha256: libcoq-bignums-ocaml_8.15.0-2_amd64.deb: OK
sha256: libcoq-bignums_8.15.0-2_amd64.deb: OK
Checksums: OK