Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/c/coq-interval/coq-interval_4.5.1-2+b1_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/coq-interval-4.5.1-2+b12fdq1qgz/coq-interval_4.5.1-2+b1_amd64.buildinfo Get source package info: coq-interval=4.5.1-2 Source URL: http://snapshot.notset.fr/mr/package/coq-interval/4.5.1-2/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.71-2 automake=1:1.16.5-1.3 autopoint=0.21-6 autotools-dev=20220109.1 base-files=12.2 base-passwd=3.5.52 bash=5.1-6.1 binutils=2.38.90.20220713-2 binutils-common=2.38.90.20220713-2 binutils-x86-64-linux-gnu=2.38.90.20220713-2 bsdextrautils=2.38-5 bsdutils=1:2.38-5 build-essential=12.9 bzip2=1.0.8-5 coq=8.15.2+dfsg-2 coreutils=8.32-4.1 cpp=4:12.1.0-3 cpp-12=12.1.0-7 dash=0.5.11+git20210903+057cd650a4ed-8 debconf=1.5.79 debhelper=13.8 debianutils=5.7-0.2 dh-autoreconf=20 dh-coq=0.3 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.13.0-1 diffutils=1:3.7-5 dpkg=1.21.9 dpkg-dev=1.21.9 dwz=0.14-1 file=1:5.41-4 findutils=4.9.0-3 g++=4:12.1.0-3 g++-12=12.1.0-7 gcc=4:12.1.0-3 gcc-12=12.1.0-7 gcc-12-base=12.1.0-7 gettext=0.21-6 gettext-base=0.21-6 grep=3.7-1 groff-base=1.22.4-8 gzip=1.12-1 hostname=3.23 init-system-helpers=1.64 intltool-debian=0.35.0+20060710.5 libacl1=2.3.1-1 libarchive-zip-perl=1.68-1 libasan8=12.1.0-7 libatomic1=12.1.0-7 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libbinutils=2.38.90.20220713-2 libblkid1=2.38-5 libbz2-1.0=1.0.8-5 libc-bin=2.33-8 libc-dev-bin=2.33-8 libc6=2.33-8 libc6-dev=2.33-8 libcap-ng0=0.8.3-1+b1 libcap2=1:2.44-1 libcc1-0=12.1.0-7 libcom-err2=1.46.5-2 libcoq-bignums=8.15.0-7 libcoq-bignums-ocaml=8.15.0-7 libcoq-coquelicot=3.2.0-7 libcoq-core-ocaml=8.15.2+dfsg-2 libcoq-core-ocaml-dev=8.15.2+dfsg-2 libcoq-flocq=4.1.0-2 libcoq-mathcomp-ssreflect=1.15.0-1 libcoq-stdlib=8.15.2+dfsg-2 libcrypt-dev=1:4.4.28-2 libcrypt1=1:4.4.28-2 libctf-nobfd0=2.38.90.20220713-2 libctf0=2.38.90.20220713-2 libdb5.3=5.3.28+dfsg1-0.10 libdebconfclient0=0.263 libdebhelper-perl=13.8 libdpkg-perl=1.21.9 libelf1=0.187-1 libexpat1=2.4.8-1 libffi8=3.4.2-4 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libgcc-12-dev=12.1.0-7 libgcc-s1=12.1.0-7 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libgmp-dev=2:6.2.1+dfsg1-1 libgmp10=2:6.2.1+dfsg1-1 libgmp3-dev=2:6.2.1+dfsg1-1 libgmpxx4ldbl=2:6.2.1+dfsg1-1 libgomp1=12.1.0-7 libgpg-error0=1.45-2 libgprofng0=2.38.90.20220713-2 libgssapi-krb5-2=1.20-1 libicu71=71.1-3 libisl23=0.25-1 libitm1=12.1.0-7 libk5crypto3=1.20-1 libkeyutils1=1.6.3-1 libkrb5-3=1.20-1 libkrb5support0=1.20-1 liblsan0=12.1.0-7 liblz4-1=1.9.3-2 liblzma5=5.2.5-2.1 libmagic-mgc=1:5.41-4 libmagic1=1:5.41-4 libmount1=2.38-5 libmpc3=1.2.1-2 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libncurses-dev=6.3+20220423-2 libncurses5-dev=6.3+20220423-2 libncurses6=6.3+20220423-2 libncursesw6=6.3+20220423-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libpam-modules=1.4.0-13 libpam-modules-bin=1.4.0-13 libpam-runtime=1.4.0-13 libpam0g=1.4.0-13 libpcre2-8-0=10.40-1 libpcre3=2:8.39-14 libperl5.34=5.34.0-5 libpipeline1=1.5.6-1 libpython3-stdlib=3.10.5-3 libpython3.10-minimal=3.10.5-1 libpython3.10-stdlib=3.10.5-1 libquadmath0=12.1.0-7 libreadline8=8.1.2-1.2 libseccomp2=2.5.4-1+b1 libselinux1=3.4-1+b1 libsigsegv2=2.14-1 libsmartcols1=2.38-5 libsqlite3-0=3.39.2-1 libssl3=3.0.5-1 libstdc++-12-dev=12.1.0-7 libstdc++6=12.1.0-7 libsub-override-perl=0.09-3 libsystemd0=251.3-1 libtinfo6=6.3+20220423-2 libtirpc-common=1.3.2-2 libtirpc-dev=1.3.2-2 libtirpc3=1.3.2-2 libtool=2.4.7-4 libtsan2=12.1.0-7 libubsan1=12.1.0-7 libuchardet0=0.0.7-1 libudev1=251.3-1 libunistring2=1.0-1 libuuid1=2.38-5 libxml2=2.9.14+dfsg-1+b1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.5.2+dfsg-1 linux-libc-dev=5.18.14-1 login=1:4.11.1+dfsg1-2 lsb-base=11.2 m4=1.4.18-5 make=4.3-4.1 man-db=2.10.2-1 mawk=1.3.4.20200120-3.1 media-types=8.0.0 ncurses-base=6.3+20220423-2 ncurses-bin=6.3+20220423-2 ocaml=4.13.1-3 ocaml-base=4.13.1-3 ocaml-compiler-libs=4.13.1-3 ocaml-findlib=1.9.3-1 ocaml-interp=4.13.1-3 ocaml-nox=4.13.1-3 patch=2.7.6-7 perl=5.34.0-5 perl-base=5.34.0-5 perl-modules-5.34=5.34.0-5 po-debconf=1.0.21+nmu1 python3=3.10.5-3 python3-minimal=3.10.5-3 python3.10=3.10.5-1 python3.10-minimal=3.10.5-1 readline-common=8.1.2-1.2 rpcsvc-proto=1.4.2-4 sed=4.8-1 sensible-utils=0.0.17 sysvinit-utils=3.03-1 tar=1.34+dfsg-1 util-linux=2.38-5 util-linux-extra=2.38-5 xz-utils=5.2.5-2.1 zlib1g=1:1.2.11.dfsg-4 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220728T094517Z/ unstable main' >> /etc/apt/sources.list && apt-get update" --customize-hook=chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash --customize-hook=chroot "$1" env sh -c "apt-get source --only-source -d coq-interval=4.5.1-2 && mkdir -p /build/coq-interval-eQtDrz && dpkg-source --no-check -x /*.dsc /build/coq-interval-eQtDrz/coq-interval-4.5.1 && cd /build/coq-interval-eQtDrz/coq-interval-4.5.1 && { printf '%s' 'coq-interval (4.5.1-2+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuild on buildd -- amd64 / i386 Build Daemon (x86-ubc-02) Wed, 27 Jul 2022 00:43:01 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-interval-eQtDrz" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-interval-eQtDrz/coq-interval-4.5.1 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658882581" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/coq-interval-eQtDrz /tmp/coq-interval-4.5.1-2+b12fdq1qgz bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220728T094517Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: null I: using /tmp/mmdebstrap.KwXiLZYqI6 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.KwXiLZYqI6 Reading package lists... Building dependency tree... util-linux is already the newest version (2.38-5). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 136 kB of archives. After this operation, 401 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20220728T094517Z unstable/main amd64 libfakeroot amd64 1.29-1 [48.5 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220728T094517Z unstable/main amd64 fakeroot amd64 1.29-1 [87.3 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 136 kB in 0s (1005 kB/s) Selecting previously unselected package libfakeroot:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 4629 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.29-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.29-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.29-1_amd64.deb ... Unpacking fakeroot (1.29-1) ... Setting up libfakeroot:amd64 (1.29-1) ... Setting up fakeroot (1.29-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.33-8) ... I: running special hook: copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220727T154516Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220728T094517Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.KwXiLZYqI6 Get:1 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm InRelease [157 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20220728T094517Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main Sources [12.1 MB] Get:4 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main amd64 Packages [11.5 MB] Fetched 23.8 MB in 19s (1228 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.KwXiLZYqI6 I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d coq-interval=4.5.1-2 && mkdir -p /build/coq-interval-eQtDrz && dpkg-source --no-check -x /*.dsc /build/coq-interval-eQtDrz/coq-interval-4.5.1 && cd /build/coq-interval-eQtDrz/coq-interval-4.5.1 && { printf '%s' 'coq-interval (4.5.1-2+b1) sid; urgency=low, binary-only=yes * Binary-only non-maintainer upload for amd64; no source changes. * Rebuild on buildd -- amd64 / i386 Build Daemon (x86-ubc-02) Wed, 27 Jul 2022 00:43:01 +0000 '; cat debian/changelog; } > debian/changelog.debrebuild && mv debian/changelog.debrebuild debian/changelog && chown -R builduser:builduser /build/coq-interval-eQtDrz"' exec /tmp/mmdebstrap.KwXiLZYqI6 Reading package lists... NOTICE: 'coq-interval' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/interval.git Please use: git clone https://salsa.debian.org/ocaml-team/interval.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 262 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-interval 4.5.1-2 (dsc) [2174 B] Get:2 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-interval 4.5.1-2 (tar) [252 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220727T154516Z bookworm/main coq-interval 4.5.1-2 (diff) [8324 B] Fetched 262 kB in 0s (983 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'coq-interval_4.5.1-2.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting coq-interval in /build/coq-interval-eQtDrz/coq-interval-4.5.1 dpkg-source: info: unpacking coq-interval_4.5.1.orig.tar.bz2 dpkg-source: info: unpacking coq-interval_4.5.1-2.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coq-interval-eQtDrz/coq-interval-4.5.1 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1658882581" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.KwXiLZYqI6 dpkg-buildpackage: info: source package coq-interval dpkg-buildpackage: info: source version 4.5.1-2+b1 dpkg-buildpackage: info: source distribution sid dpkg-buildpackage: info: source changed by amd64 / i386 Build Daemon (x86-ubc-02) dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with coq dh_clean debian/rules binary-arch dh binary-arch --with coq dh_update_autotools_config -a dh_autoreconf -a autoreconf: warning: autoconf input should be named 'configure.ac', not 'configure.in' aclocal: warning: autoconf input should be named 'configure.ac', not 'configure.in' configure.in:5: warning: prefer named diversions dh_auto_configure -a ./configure --build=x86_64-linux-gnu --prefix=/usr --includedir=\${prefix}/include --mandir=\${prefix}/share/man --infodir=\${prefix}/share/info --sysconfdir=/etc --localstatedir=/var --disable-option-checking --disable-silent-rules --libdir=\${prefix}/lib/x86_64-linux-gnu --runstatedir=/run --disable-maintainer-mode --disable-dependency-tracking checking for gcc... gcc checking whether the C compiler works... yes checking for C compiler default output file name... a.out checking for suffix of executables... checking whether we are cross compiling... no checking for suffix of object files... o checking whether the compiler supports GNU C... yes checking whether gcc accepts -g... yes checking for gcc option to enable C11 features... none needed checking how to run the C preprocessor... gcc -E checking for coqc... /usr/bin/coqc checking Coq version... 81502 checking for coqdep... /usr/bin/coqdep checking for coqdoc... /usr/bin/coqdoc checking for ocamlfind... /usr/bin/ocamlfind checking for Flocq... yes checking for primitive floats... yes checking for Ssreflect... yes checking for Coquelicot... yes checking for Bignums... yes checking for native development files... yes checking for bytecode development files... yes checking for g++... g++ checking whether the compiler supports GNU C++... yes checking whether g++ accepts -g... yes checking for g++ option to enable C++11 features... none needed configure: building remake... /usr/bin/ld: /tmp/ccEhUBHQ.o: in function `main': remake.cpp:(.text.startup+0xbab): warning: the use of `tempnam' is dangerous, better use `mkstemp' === Summary === Installation directory /usr/lib/ocaml/coq/user-contrib Plot tactic native bytecode configure: creating ./config.status config.status: creating Remakefile debian/rules override_dh_auto_build make[1]: Entering directory '/build/coq-interval-eQtDrz/coq-interval-4.5.1' ./remake Building src/Tactic_float.v Finished src/Tactic_float.v Building src/Tactic.vo Building src/Float/Sig.vo Building src/Float/Basic.vo Building src/Real/Xreal.vo Building src/Missing/Stdlib.vo File "./src/Missing/Stdlib.v", line 1085, characters 0-37: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Missing/Stdlib.vo File "./src/Real/Xreal.v", line 186, characters 0-31: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope XR_scope.". [undeclared-scope,deprecated] Finished src/Real/Xreal.vo Finished src/Float/Basic.vo Finished src/Float/Sig.vo Building src/Float/Specific_bigint.vo Building src/Float/Generic.vo Finished src/Float/Generic.vo Building src/Float/Generic_proof.vo Finished src/Float/Generic_proof.vo Building src/Float/Specific_sig.vo Finished src/Float/Specific_sig.vo Finished src/Float/Specific_bigint.vo Building src/Float/Specific_ops.vo Finished src/Float/Specific_ops.vo Building src/Interval/Float_full.vo Building src/Interval/Float.vo Building src/Interval/Interval.vo File "./src/Interval/Interval.v", line 21, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Interval/Interval.vo Finished src/Interval/Float.vo Building src/Interval/Transcend.vo File "./src/Interval/Transcend.v", line 52, characters 0-88: Warning: Not a truly recursive cofixpoint. [non-recursive,fixpoints] Finished src/Interval/Transcend.vo Finished src/Interval/Float_full.vo Building src/Tactic_float.vo Building src/Float/Primitive_ops.vo File "./src/Float/Primitive_ops.v", line 39, characters 12-20: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 39, characters 22-34: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 44, characters 15-23: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 44, characters 25-37: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 54, characters 12-20: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 54, characters 22-34: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 60, characters 6-11: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 60, characters 13-21: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 60, characters 23-33: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 60, characters 23-27: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 64, characters 15-23: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 64, characters 25-37: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 70, characters 15-20: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 70, characters 24-32: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 70, characters 34-38: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 79, characters 12-20: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 79, characters 22-34: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 85, characters 17-22: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 85, characters 24-32: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 85, characters 34-38: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 89, characters 15-23: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 89, characters 25-37: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 95, characters 6-11: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 95, characters 15-23: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 95, characters 25-41: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 95, characters 25-35: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 106, characters 15-23: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 106, characters 25-37: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 107, characters 15-25: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 135, characters 3-13: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 170, characters 16-56: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 170, characters 16-26: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 170, characters 31-41: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 197, characters 7-16: Warning: Notation Int63.leb is deprecated since 8.14. Use Uint63.leb instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 197, characters 18-22: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 199, characters 16-57: Warning: Notation "_ - _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 199, characters 16-20: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 200, characters 17-23: Warning: Notation "_ >> _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 202, characters 66-74: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 202, characters 41-49: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 208, characters 10-18: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 205, characters 25-33: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 206, characters 42-50: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 206, characters 52-58: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 213, characters 21-29: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 214, characters 38-46: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 214, characters 48-54: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 211, characters 25-33: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 216, characters 18-26: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 220, characters 21-29: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 220, characters 31-37: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 222, characters 30-39: Warning: Notation "_ land _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 222, characters 56-64: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 222, characters 66-72: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 222, characters 30-39: Warning: Notation "_ land _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 222, characters 56-64: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 222, characters 66-72: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 333, characters 3-13: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 334, characters 7-15: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 334, characters 33-43: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 339, characters 52-62: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 339, characters 52-62: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 346, characters 33-45: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 346, characters 33-45: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 349, characters 46-58: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 349, characters 46-58: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 359, characters 7-15: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 359, characters 17-29: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 362, characters 13-23: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 362, characters 25-31: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 362, characters 13-23: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 362, characters 25-31: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 363, characters 11-23: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 363, characters 33-43: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 363, characters 11-23: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 363, characters 33-43: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 364, characters 10-19: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 364, characters 10-19: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 364, characters 10-19: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 440, characters 47-55: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 440, characters 47-55: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 444, characters 48-56: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 444, characters 48-56: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 445, characters 41-49: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 445, characters 41-49: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 446, characters 34-42: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 446, characters 34-42: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 448, characters 47-55: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 448, characters 47-55: Warning: Notation pow2_pos is deprecated since 8.14. Use Uint63.pow2_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 476, characters 34-42: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 476, characters 44-50: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 476, characters 34-42: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 476, characters 44-50: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 487, characters 28-33: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 487, characters 28-33: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 487, characters 28-33: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 491, characters 19-29: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 491, characters 31-41: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 491, characters 31-35: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 491, characters 19-29: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 491, characters 31-41: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 491, characters 31-35: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 492, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 492, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 492, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 492, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 12-26: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 48-54: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 12-26: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 12-26: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 48-54: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 48-54: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 48-54: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 494, characters 48-54: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 495, characters 23-41: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 495, characters 43-47: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 495, characters 23-41: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 495, characters 43-47: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 501, characters 17-27: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 501, characters 29-39: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 501, characters 29-33: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 501, characters 17-27: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 501, characters 29-39: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 501, characters 29-33: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 538, characters 32-40: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 538, characters 42-48: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 538, characters 32-40: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 538, characters 42-48: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 557, characters 20-28: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 557, characters 30-34: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 557, characters 20-28: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 557, characters 30-34: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 559, characters 10-16: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 559, characters 10-16: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 559, characters 10-16: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 559, characters 10-16: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 625, characters 34-42: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 625, characters 44-50: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 625, characters 34-42: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 625, characters 44-50: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 640, characters 21-29: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 640, characters 31-35: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 640, characters 21-29: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 640, characters 31-35: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 641, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 641, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 641, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 641, characters 28-34: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 644, characters 23-41: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 644, characters 43-47: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 644, characters 23-41: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 644, characters 43-47: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 698, characters 34-42: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 698, characters 44-50: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 698, characters 34-42: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 698, characters 44-50: Warning: Notation of_pos is deprecated since 8.14. Use Uint63.of_pos instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 710, characters 26-31: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 710, characters 26-31: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 710, characters 26-31: Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 717, characters 17-27: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 717, characters 29-39: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 717, characters 29-33: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 717, characters 17-27: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 717, characters 29-39: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 717, characters 29-33: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 718, characters 26-32: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 718, characters 26-32: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 718, characters 26-32: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 718, characters 26-32: Warning: Notation is_int is deprecated since 8.14. Use Uint63.is_int instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 10-24: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 46-52: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 10-24: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 10-24: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 46-52: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 46-52: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 46-52: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 720, characters 46-52: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 721, characters 21-39: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 721, characters 41-45: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 721, characters 21-39: Warning: Notation to_Z_bounded is deprecated since 8.14. Use Uint63.to_Z_bounded instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 721, characters 41-45: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 727, characters 15-25: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 727, characters 27-37: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 727, characters 27-31: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 727, characters 15-25: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 727, characters 27-37: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 727, characters 27-31: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2548, characters 0-13: Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2548, characters 0-13: Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2558, characters 5-9: Warning: Notation lebP is deprecated since 8.14. Use Uint63.lebP instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2559, characters 12-16: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2558, characters 5-9: Warning: Notation lebP is deprecated since 8.14. Use Uint63.lebP instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2559, characters 12-16: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2559, characters 12-16: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2578, characters 16-20: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2578, characters 16-20: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2579, characters 9-20: Warning: Notation "_ - _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2579, characters 9-13: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2580, characters 8-12: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2580, characters 31-35: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2579, characters 9-20: Warning: Notation "_ - _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2579, characters 9-13: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2580, characters 8-12: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2580, characters 31-35: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 10-24: Warning: Notation to_Z_inj is deprecated since 8.14. Use Uint63.to_Z_inj instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 34-48: Warning: Notation Int63.sub_spec is deprecated since 8.14. Use Uint63.sub_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 50-65: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 10-24: Warning: Notation to_Z_inj is deprecated since 8.14. Use Uint63.to_Z_inj instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 34-48: Warning: Notation Int63.sub_spec is deprecated since 8.14. Use Uint63.sub_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 34-48: Warning: Notation Int63.sub_spec is deprecated since 8.14. Use Uint63.sub_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 50-65: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2581, characters 50-65: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2583, characters 10-14: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2583, characters 16-20: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2583, characters 10-14: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2583, characters 16-20: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2586, characters 13-17: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2586, characters 13-17: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2589, characters 26-34: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2589, characters 26-34: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2589, characters 26-34: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2590, characters 26-34: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2590, characters 36-41: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2590, characters 26-34: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2590, characters 36-41: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2590, characters 26-34: Warning: Notation of_int63 is deprecated since 8.14. Use of_uint63 instead. [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2590, characters 36-41: Warning: Notation "_ + _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 15-25: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 27-82: Warning: Notation "_ land _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 27-75: Warning: Notation "_ >> _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 49-53: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 15-25: Warning: Notation to_Z is deprecated since 8.14. Use Uint63.to_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 27-82: Warning: Notation "_ land _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 27-75: Warning: Notation "_ >> _" is deprecated since 8.14. Use the uint63_scope instead. [deprecated-notation,deprecated] File "./src/Float/Primitive_ops.v", line 2592, characters 49-53: Warning: Notation of_Z is deprecated since 8.14. Use Uint63.of_Z instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2593, characters 13-23: Warning: Notation eqbP is deprecated since 8.14. Use Uint63.eqbP instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2593, characters 13-23: Warning: Notation eqbP is deprecated since 8.14. Use Uint63.eqbP instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2594, characters 8-24: Warning: Notation land_spec' is deprecated since 8.14. Use Uint63.land_spec' instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2594, characters 26-38: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2594, characters 8-24: Warning: Notation land_spec' is deprecated since 8.14. Use Uint63.land_spec' instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2594, characters 8-24: Warning: Notation land_spec' is deprecated since 8.14. Use Uint63.land_spec' instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2594, characters 26-38: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2594, characters 26-38: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2595, characters 25-39: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2595, characters 42-50: Warning: Notation lsr_spec is deprecated since 8.14. Use Uint63.lsr_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2595, characters 25-39: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2595, characters 25-39: Warning: Notation Int63.add_spec is deprecated since 8.14. Use Uint63.add_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2595, characters 42-50: Warning: Notation lsr_spec is deprecated since 8.14. Use Uint63.lsr_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2595, characters 42-50: Warning: Notation lsr_spec is deprecated since 8.14. Use Uint63.lsr_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2595, characters 42-50: Warning: Notation lsr_spec is deprecated since 8.14. Use Uint63.lsr_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2596, characters 8-14: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2596, characters 8-14: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2596, characters 8-14: Warning: Notation to_Z_1 is deprecated since 8.14. Use Uint63.to_Z_1 instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2602, characters 8-17: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2602, characters 8-17: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2602, characters 8-17: Warning: Notation of_Z_spec is deprecated since 8.14. Use Uint63.of_Z_spec instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2753, characters 22-29: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2753, characters 22-29: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2781, characters 41-48: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2781, characters 41-48: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2824, characters 43-50: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2824, characters 43-50: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2832, characters 20-27: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2832, characters 20-27: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2844, characters 22-29: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2844, characters 22-29: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2852, characters 20-27: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] File "./src/Float/Primitive_ops.v", line 2852, characters 20-27: Warning: Notation pow2_nz is deprecated since 8.14. Use Uint63.pow2_nz instead [deprecated-syntactic-definition,deprecated] Finished src/Float/Primitive_ops.vo Finished src/Tactic_float.vo Building src/Tactics/Integral_helper.vo Building src/Eval/Eval.vo Building src/Eval/Prog.vo Building src/Eval/Tree.vo Finished src/Eval/Tree.vo Finished src/Eval/Prog.vo Building src/Interval/Interval_compl.vo Building src/Missing/MathComp.vo File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/MathComp.v", line 24, characters 0-88: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Missing/MathComp.vo Building src/Real/Taylor.vo File "./src/Real/Taylor.v", line 24, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Real/Taylor.vo File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 24, characters 0-84: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Interval/Interval_compl.v", line 25, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Interval/Interval_compl.vo Building src/Missing/Coquelicot.vo File "./src/Missing/Coquelicot.v", line 22, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 23, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Missing/Coquelicot.v", line 494, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 497, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 515, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 529, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 532, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Missing/Coquelicot.v", line 551, characters 0-17: Warning: Duplicate clear of x [duplicate-clear,ssr] Finished src/Missing/Coquelicot.vo Building src/Poly/Taylor_model.vo Building src/Interval/Univariate_sig.vo Finished src/Interval/Univariate_sig.vo Building src/Poly/Bound.vo Building src/Poly/Datatypes.vo Building src/Poly/Basic_rec.vo File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Basic_rec.v", line 24, characters 0-102: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Basic_rec.vo File "./src/Poly/Datatypes.v", line 24, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 25, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Datatypes.v", line 852, characters 0-70: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope ipoly_scope.". [undeclared-scope,deprecated] File "./src/Poly/Datatypes.v", line 989, characters 0-34: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope ipoly_scope.". [undeclared-scope,deprecated] Finished src/Poly/Datatypes.vo File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound.v", line 24, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Bound.vo Building src/Poly/Bound_quad.vo File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Bound_quad.v", line 25, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Bound_quad.vo Building src/Poly/Taylor_model_sharp.vo Building src/Poly/Taylor_poly.vo File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_poly.v", line 26, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Taylor_poly.vo Building src/Real/Xreal_derive.vo Finished src/Real/Xreal_derive.vo File "./src/Poly/Taylor_model_sharp.v", line 25, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 26, characters 0-96: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model_sharp.v", line 1348, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1357, characters 2-76: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1580, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1682, characters 6-32: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1720, characters 4-48: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1742, characters 4-53: Warning: Duplicate clear of X [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1751, characters 2-28: Warning: Duplicate clear of E0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1853, characters 4-48: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 1961, characters 4-48: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2053, characters 2-51: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2168, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2310, characters 4-37: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2421, characters 2-189: Warning: Duplicate clear of X [duplicate-clear,ssr] File "./src/Poly/Taylor_model_sharp.v", line 2424, characters 4-45: Warning: Duplicate clear of X0 [duplicate-clear,ssr] Finished src/Poly/Taylor_model_sharp.vo File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Poly/Taylor_model.v", line 21, characters 0-88: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Poly/Taylor_model.vo File "./src/Eval/Eval.v", line 23, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Eval/Eval.v", line 522, characters 0-25: Warning: Duplicate clear of H [duplicate-clear,ssr] Finished src/Eval/Eval.vo Building src/Eval/Reify.vo Finished src/Eval/Reify.vo Building src/Integral/Bertrand.vo File "./src/Integral/Bertrand.v", line 3, characters 0-53: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing] File "./src/Integral/Bertrand.v", line 4, characters 0-77: Warning: Notation "_ ^ _" was already used in scope nat_scope. [notation-overridden,parsing] Finished src/Integral/Bertrand.vo Building src/Integral/Integral.vo File "./src/Integral/Integral.v", line 21, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./src/Integral/Integral.v", line 583, characters 2-57: Warning: Duplicate clear of HPint [duplicate-clear,ssr] File "./src/Integral/Integral.v", line 742, characters 2-57: Warning: Duplicate clear of HPint [duplicate-clear,ssr] Finished src/Integral/Integral.vo Building src/Integral/Refine.vo Building src/Integral/Priority.vo File "./src/Integral/Priority.v", line 527, characters 0-118: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] Finished src/Integral/Priority.vo File "./src/Integral/Refine.v", line 21, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Integral/Refine.vo Building src/Tactics/Interval_helper.vo Finished src/Tactics/Interval_helper.vo File "./src/Tactics/Integral_helper.v", line 22, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Tactics/Integral_helper.vo Building src/Tactics/Plot_helper.vo Finished src/Tactics/Plot_helper.vo Building src/Tactics/Root_helper.vo Finished src/Tactics/Root_helper.vo File "./src/Tactic.v", line 22, characters 0-42: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished src/Tactic.vo Building src/Float/Generic_ops.vo Finished src/Float/Generic_ops.vo Building src/Float/Specific_stdz.vo Finished src/Float/Specific_stdz.vo Building src/Plot/interval_plot.ml Finished src/Plot/interval_plot.ml Building src/Plot/interval_plot.cmxs File "src/Plot/plot.c", line 22, characters 45-76: Alert deprecated: Coqlib.gen_reference_in_modules Please use Coqlib.lib_ref File "src/Plot/plot.c", line 147, characters 34-40: Warning 20 [ignored-extra-argument]: this argument will not be used by the function. File "src/Plot/plot.c", line 151, characters 28-34: Warning 20 [ignored-extra-argument]: this argument will not be used by the function. Finished src/Plot/interval_plot.cmxs Building src/Plot/interval_plot.cmo File "src/Plot/plot.c", line 22, characters 45-76: Alert deprecated: Coqlib.gen_reference_in_modules Please use Coqlib.lib_ref File "src/Plot/plot.c", line 147, characters 34-40: Warning 20 [ignored-extra-argument]: this argument will not be used by the function. File "src/Plot/plot.c", line 151, characters 28-34: Warning 20 [ignored-extra-argument]: this argument will not be used by the function. Finished src/Plot/interval_plot.cmo Building src/Plot.vo Finished src/Plot.vo Building all Finished all make[1]: Leaving directory '/build/coq-interval-eQtDrz/coq-interval-4.5.1' create-stamp debian/debhelper-build-stamp dh_prep -a debian/rules override_dh_auto_install make[1]: Entering directory '/build/coq-interval-eQtDrz/coq-interval-4.5.1' DESTDIR=/build/coq-interval-eQtDrz/coq-interval-4.5.1/debian/tmp ./remake install Building install Finished install make[1]: Leaving directory '/build/coq-interval-eQtDrz/coq-interval-4.5.1' dh_install -a dh_installdocs -a dh_installchangelogs -a dh_installexamples -a dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a dh_missing -a dh_dwz -a dwz: debian/libcoq-interval/usr/lib/ocaml/coq/user-contrib/Interval/interval_plot.cmxs: .debug_info section not present dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_coq -a dh_gencontrol -a dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libcoq-interval' in '../libcoq-interval_4.5.1-2+b1_amd64.deb'. dpkg-deb: building package 'libcoq-interval-dbgsym' in '../libcoq-interval-dbgsym_4.5.1-2+b1_amd64.deb'. dpkg-genbuildinfo --build=any -O../coq-interval_4.5.1-2+b1_amd64.buildinfo dpkg-genchanges --build=any -O../coq-interval_4.5.1-2+b1_amd64.changes dpkg-genchanges: info: binary-only arch-specific upload (source code and arch-indep packages not included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: running special hook: sync-out /build/coq-interval-eQtDrz /tmp/coq-interval-4.5.1-2+b12fdq1qgz I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap.KwXiLZYqI6... I: success in 1069.1617 seconds md5: libcoq-interval-dbgsym_4.5.1-2+b1_amd64.deb: OK md5: Value of 'md5' differs for libcoq-interval_4.5.1-2+b1_amd64.deb md5: Size differs for libcoq-interval_4.5.1-2+b1_amd64.deb sha1: libcoq-interval-dbgsym_4.5.1-2+b1_amd64.deb: OK sha1: Value of 'sha1' differs for libcoq-interval_4.5.1-2+b1_amd64.deb sha1: Size differs for libcoq-interval_4.5.1-2+b1_amd64.deb sha256: libcoq-interval-dbgsym_4.5.1-2+b1_amd64.deb: OK sha256: Value of 'sha256' differs for libcoq-interval_4.5.1-2+b1_amd64.deb sha256: Size differs for libcoq-interval_4.5.1-2+b1_amd64.deb Checksums: FAIL Cannot generate diffoscope for libcoq-interval_4.5.1-2+b1_amd64.deb: RetryError[]