Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/m/mathcomp-zify/mathcomp-zify_1.2.0+1.12+8.13-3_amd64.buildinfo
Use metasnap for getting required timestamps
New buildinfo file: /tmp/mathcomp-zify-1.2.0+1.12+8.13-3m32ee_hj/mathcomp-zify_1.2.0+1.12+8.13-3_amd64.buildinfo
Get source package info: mathcomp-zify=1.2.0+1.12+8.13-3
Source URL: http://snapshot.notset.fr/mr/package/mathcomp-zify/1.2.0+1.12+8.13-3/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-3 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-3 gcc=4:11.2.0-2 gcc-11=11.3.0-3 gcc-11-base=11.3.0-3 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-3 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-mathcomp-algebra=1.14.0-10 libcoq-mathcomp-fingroup=1.14.0-10 libcoq-mathcomp-ssreflect=1.14.0-10 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-3 libgcc-s1=12.1.0-2 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libgmp10=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-5 libstdc++-11-dev=11.3.0-3 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-3 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 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/20220528T035722Z/ bookworm main
deb-src http://snapshot.notset.fr/archive/debian/20220528T035722Z/ bookworm main
deb http://snapshot.notset.fr/archive/debian/20220523T090707Z/ 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 mathcomp-zify=1.2.0+1.12+8.13-3 && mkdir -p /build/mathcomp-zify-vHOlOU && dpkg-source --no-check -x /*.dsc /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13 && chown -R builduser:builduser /build/mathcomp-zify-vHOlOU" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1653306530" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/mathcomp-zify-vHOlOU /tmp/mathcomp-zify-1.2.0+1.12+8.13-3m32ee_hj bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220523T090707Z 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.E8x5oZIN3e 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.E8x5oZIN3e
Reading package lists...
Building dependency tree...
util-linux is already the newest version (2.38-4).
The following NEW packages will be installed:
  fakeroot libfakeroot
0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded.
Need to get 136 kB of archives.
After this operation, 401 kB of additional disk space will be used.
Get:1 http://snapshot.notset.fr/archive/debian/20220523T090707Z unstable/main amd64 libfakeroot amd64 1.29-1 [48.5 kB]
Get:2 http://snapshot.notset.fr/archive/debian/20220523T090707Z unstable/main amd64 fakeroot amd64 1.29-1 [87.3 kB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 136 kB in 0s (1084 kB/s)
Selecting previously unselected package libfakeroot:amd64.
(Reading database ... 
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 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-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/20220528T035722Z/ bookworm main
deb-src http://snapshot.notset.fr/archive/debian/20220528T035722Z/ bookworm main
deb http://snapshot.notset.fr/archive/debian/20220523T090707Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.E8x5oZIN3e
Get:1 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm InRelease [130 kB]
Hit:2 http://snapshot.notset.fr/archive/debian/20220523T090707Z unstable InRelease
Ign:3 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main Sources
Ign:4 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main amd64 Packages
Ign:3 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main Sources
Ign:4 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main amd64 Packages
Ign:3 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main Sources
Ign:4 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main amd64 Packages
Get:3 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main Sources [12.0 MB]
Get:4 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main amd64 Packages [11.5 MB]
Fetched 23.5 MB in 19s (1211 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.E8x5oZIN3e
I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d mathcomp-zify=1.2.0+1.12+8.13-3 && mkdir -p /build/mathcomp-zify-vHOlOU && dpkg-source --no-check -x /*.dsc /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13 && chown -R builduser:builduser /build/mathcomp-zify-vHOlOU"' exec /tmp/mmdebstrap.E8x5oZIN3e
Reading package lists...
NOTICE: 'mathcomp-zify' packaging is maintained in the 'Git' version control system at:
https://salsa.debian.org/ocaml-team/mathcomp-zify.git
Please use:
git clone https://salsa.debian.org/ocaml-team/mathcomp-zify.git
to retrieve the latest (possibly unreleased) updates to the package.
Need to get 30.9 kB of source archives.
Get:1 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main mathcomp-zify 1.2.0+1.12+8.13-3 (dsc) [2105 B]
Get:2 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main mathcomp-zify 1.2.0+1.12+8.13-3 (tar) [20.3 kB]
Get:3 http://snapshot.notset.fr/archive/debian/20220528T035722Z bookworm/main mathcomp-zify 1.2.0+1.12+8.13-3 (diff) [8448 B]
Fetched 30.9 kB in 0s (502 kB/s)
Download complete and in download only mode
W: Download is performed unsandboxed as root as file 'mathcomp-zify_1.2.0+1.12+8.13-3.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied)
dpkg-source: info: extracting mathcomp-zify in /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13
dpkg-source: info: unpacking mathcomp-zify_1.2.0+1.12+8.13.orig.tar.gz
dpkg-source: info: unpacking mathcomp-zify_1.2.0+1.12+8.13-3.debian.tar.xz
I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1653306530" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.E8x5oZIN3e
dpkg-buildpackage: info: source package mathcomp-zify
dpkg-buildpackage: info: source version 1.2.0+1.12+8.13-3
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 distclean
make[1]: Entering directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
rm -f Makefile.coq Makefile.coq.conf
rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf
make[1]: Leaving directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
   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/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
make
make[2]: Entering directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
coq_makefile -f Make -o Makefile.coq
make --no-print-directory -f Makefile.coq 
COQDEP VFILES
COQC theories/zify_ssreflect.v
File "./theories/zify_ssreflect.v", line 18, characters 0-89:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 22, characters 0-59:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 29, characters 0-103:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 33, characters 0-88:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 37, characters 0-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 "./theories/zify_ssreflect.v", line 40, characters 0-115:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 44, characters 0-65:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 47, characters 0-123:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 51, characters 0-65:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 54, characters 0-122:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 58, characters 0-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 "./theories/zify_ssreflect.v", line 61, characters 0-122:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 65, characters 0-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 "./theories/zify_ssreflect.v", line 68, characters 0-120:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 72, characters 0-139:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 77, 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]
File "./theories/zify_ssreflect.v", line 81, characters 0-138:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 86, characters 0-77:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 89, characters 0-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 "./theories/zify_ssreflect.v", line 92, characters 0-76:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 95, characters 0-68:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 98, characters 0-57:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 101, characters 0-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 "./theories/zify_ssreflect.v", line 104, 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 "./theories/zify_ssreflect.v", line 107, 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 "./theories/zify_ssreflect.v", line 110, characters 0-129:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 114, characters 0-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 "./theories/zify_ssreflect.v", line 121, characters 0-42:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 124, characters 0-58:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 127, 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 "./theories/zify_ssreflect.v", line 130, characters 0-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 "./theories/zify_ssreflect.v", line 133, characters 0-114:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 137, characters 0-48:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 140, characters 0-40:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 143, characters 0-48:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 146, characters 0-40:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 149, characters 0-114:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 153, characters 0-88:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 157, characters 0-104:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 161, characters 0-104:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 165, characters 0-104:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 169, characters 0-92:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 173, characters 0-92:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 177, characters 0-93:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 181, characters 0-99:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 185, characters 0-121:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 192, characters 0-90:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 196, characters 0-45:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 199, characters 0-114:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 203, characters 0-114:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 213, characters 0-110:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 217, characters 0-97:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 224, characters 0-142:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 229, characters 0-121:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 233, 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 "./theories/zify_ssreflect.v", line 236, characters 0-59:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 239, 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 "./theories/zify_ssreflect.v", line 242, characters 0-59:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 245, 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 "./theories/zify_ssreflect.v", line 248, characters 0-58:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 251, 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 "./theories/zify_ssreflect.v", line 254, characters 0-58:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 257, 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 "./theories/zify_ssreflect.v", line 260, characters 0-137:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 264, 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 "./theories/zify_ssreflect.v", line 267, characters 0-137:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 271, characters 0-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 "./theories/zify_ssreflect.v", line 274, characters 0-67:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 277, characters 0-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 "./theories/zify_ssreflect.v", line 280, characters 0-67:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 283, 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 "./theories/zify_ssreflect.v", line 303, characters 0-72:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 306, characters 0-72:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 379, characters 0-79:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 382, characters 0-100:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 386, characters 0-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 "./theories/zify_ssreflect.v", line 390, characters 0-110:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 394, characters 0-128:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 399, characters 0-98:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 403, characters 0-115:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 420, characters 0-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 "./theories/zify_ssreflect.v", line 432, characters 0-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 "./theories/zify_ssreflect.v", line 435, characters 0-124:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 444, characters 0-61:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 447, 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 "./theories/zify_ssreflect.v", line 450, characters 0-142:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 454, characters 0-71:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 457, characters 0-180:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 462, characters 0-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 "./theories/zify_ssreflect.v", line 465, characters 0-180:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 470, characters 0-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 "./theories/zify_ssreflect.v", line 473, characters 0-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 "./theories/zify_ssreflect.v", line 476, characters 0-73:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 479, characters 0-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 "./theories/zify_ssreflect.v", line 482, characters 0-73:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 485, characters 0-88:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 489, characters 0-72:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_ssreflect.v", line 492, 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 "./theories/zify_ssreflect.v", line 495, characters 0-57:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC theories/ssrZ.v
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
File "./theories/ssrZ.v", line 5, characters 0-74:
Warning:
New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
COQC theories/zify_algebra.v
File "./theories/zify_algebra.v", line 6, characters 0-78:
Warning:
New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
File "./theories/zify_algebra.v", line 6, characters 0-78:
Warning:
New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
File "./theories/zify_algebra.v", line 6, characters 0-78:
Warning:
New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
File "./theories/zify_algebra.v", line 6, characters 0-78:
Warning:
New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
File "./theories/zify_algebra.v", line 6, characters 0-78:
Warning:
New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
File "./theories/zify_algebra.v", line 6, characters 0-78:
Warning:
New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
File "./theories/zify_algebra.v", line 6, characters 0-78:
Warning:
New coercion path [GRing.Pred.subring_smul; GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
File "./theories/zify_algebra.v", line 24, characters 0-88:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 28, characters 0-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 "./theories/zify_algebra.v", line 31, characters 0-77:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 34, characters 0-67:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 37, characters 0-92:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 41, characters 0-113:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 45, characters 0-160:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 50, characters 0-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 "./theories/zify_algebra.v", line 53, characters 0-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 "./theories/zify_algebra.v", line 56, characters 0-43:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 59, characters 0-79:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 62, 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 "./theories/zify_algebra.v", line 65, characters 0-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 "./theories/zify_algebra.v", line 68, characters 0-83:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 72, characters 0-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 "./theories/zify_algebra.v", line 75, characters 0-145:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 79, characters 0-130:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 83, characters 0-84:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 90, characters 0-118:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 94, characters 0-149:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 98, characters 0-67:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 101, characters 0-81:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 105, characters 0-48:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 108, characters 0-88:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 112, characters 0-121:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 116, characters 0-103:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 120, characters 0-103:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 124, characters 0-113:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 128, characters 0-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 "./theories/zify_algebra.v", line 131, characters 0-42:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 134, characters 0-59:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 137, characters 0-108:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 141, 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 "./theories/zify_algebra.v", line 144, characters 0-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 "./theories/zify_algebra.v", line 147, characters 0-58:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 150, characters 0-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 "./theories/zify_algebra.v", line 154, characters 0-61:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 157, characters 0-127:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 161, characters 0-143:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 165, characters 0-127:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 169, characters 0-143:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 173, characters 0-129:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 177, characters 0-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 "./theories/zify_algebra.v", line 180, characters 0-129:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 184, characters 0-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 "./theories/zify_algebra.v", line 191, characters 0-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 "./theories/zify_algebra.v", line 194, characters 0-71:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 197, characters 0-91:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 201, characters 0-92:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 205, characters 0-71:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 208, characters 0-93:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 215, 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]
File "./theories/zify_algebra.v", line 219, characters 0-136:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 223, characters 0-78:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 229, characters 0-110:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 233, characters 0-136:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 237, characters 0-77:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 240, characters 0-78:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 243, characters 0-86:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 247, characters 0-90:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 251, characters 0-101:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 255, characters 0-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 "./theories/zify_algebra.v", line 259, 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 "./theories/zify_algebra.v", line 262, characters 0-102:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 266, 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 "./theories/zify_algebra.v", line 269, characters 0-93:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 273, 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 "./theories/zify_algebra.v", line 276, characters 0-101:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 280, 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 "./theories/zify_algebra.v", line 283, 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]
File "./theories/zify_algebra.v", line 287, characters 0-133:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 291, 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]
File "./theories/zify_algebra.v", line 295, characters 0-133:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 299, characters 0-121:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 303, characters 0-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 "./theories/zify_algebra.v", line 306, characters 0-121:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 310, characters 0-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 "./theories/zify_algebra.v", line 321, characters 0-103:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 325, characters 0-93:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 329, characters 0-122:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
File "./theories/zify_algebra.v", line 338, characters 0-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 "./theories/zify_algebra.v", line 341, characters 0-127:
Warning: The default value for instance locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]
COQC theories/zify.v
make[2]: Leaving directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
make[1]: Leaving directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
dh: command-omitted: The call to "debian/rules override_dh_auto_test" 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/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
make install DESTDIR=/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp
make[2]: Entering directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
coq_makefile -f Make -o Makefile.coq
make --no-print-directory -f Makefile.coq install
INSTALL theories/ssrZ.vo /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify_ssreflect.vo /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify_algebra.vo /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify.vo /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/ssrZ.v /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify_ssreflect.v /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify_algebra.v /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify.v /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/ssrZ.glob /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify_ssreflect.glob /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify_algebra.glob /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
INSTALL theories/zify.glob /build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/zify/
make[2]: Leaving directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
make[1]: Leaving directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
   dh_install -a
   dh_ocamldoc -a
   dh_installdocs -a
   dh_installchangelogs -a
   dh_installexamples -a
   dh_perl -a
   dh_link -a
   dh_strip_nondeterminism -a
   dh_compress -a
   dh_fixperms -a
   dh_missing -a
   dh_strip -a
   dh_makeshlibs -a
   dh_shlibdeps -a
   dh_installdeb -a
   dh_ocaml -a
   debian/rules override_dh_gencontrol
make[1]: Entering directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
dh_gencontrol -- -VF:CoqABI="8.15.1+4.13.1"
dpkg-gencontrol: warning: Provides field of package libcoq-mathcomp-zify: substitution variable ${ocaml:Provides} used, but is not defined
make[1]: Leaving directory '/build/mathcomp-zify-vHOlOU/mathcomp-zify-1.2.0+1.12+8.13'
   dh_md5sums -a
   dh_builddeb -a
dpkg-deb: building package 'libcoq-mathcomp-zify' in '../libcoq-mathcomp-zify_1.2.0+1.12+8.13-3_amd64.deb'.
 dpkg-genbuildinfo --build=any -O../mathcomp-zify_1.2.0+1.12+8.13-3_amd64.buildinfo
 dpkg-genchanges --build=any -O../mathcomp-zify_1.2.0+1.12+8.13-3_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/mathcomp-zify-vHOlOU /tmp/mathcomp-zify-1.2.0+1.12+8.13-3m32ee_hj
I: cleaning package lists and apt cache...
I: removing tempdir /tmp/mmdebstrap.E8x5oZIN3e...
I: success in 668.9043 seconds
md5: libcoq-mathcomp-zify_1.2.0+1.12+8.13-3_amd64.deb: OK
sha1: libcoq-mathcomp-zify_1.2.0+1.12+8.13-3_amd64.deb: OK
sha256: libcoq-mathcomp-zify_1.2.0+1.12+8.13-3_amd64.deb: OK
Checksums: OK