Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/c/coquelicot/coquelicot_3.2.0-7_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/coquelicot-3.2.0-7yn9nffpe/coquelicot_3.2.0-7_amd64.buildinfo Get source package info: coquelicot=3.2.0-7 Source URL: http://snapshot.notset.fr/mr/package/coquelicot/3.2.0-7/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.71-2 automake=1:1.16.5-1.3 autopoint=0.21-6 autotools-dev=20220109.1 base-files=12.2 base-passwd=3.5.52 bash=5.1-6.1 binutils=2.38.50.20220629-4 binutils-common=2.38.50.20220629-4 binutils-x86-64-linux-gnu=2.38.50.20220629-4 bsdextrautils=2.38-4 bsdutils=1:2.38-4 build-essential=12.9 bzip2=1.0.8-5 coq=8.15.2+dfsg-2 coreutils=8.32-4.1 cpp=4:11.2.0-2 cpp-11=11.3.0-4 dash=0.5.11+git20210903+057cd650a4ed-8 debconf=1.5.79 debhelper=13.8 debianutils=5.7-0.2 dh-autoreconf=20 dh-coq=0.3 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.13.0-1 diffutils=1:3.7-5 dpkg=1.21.9 dpkg-dev=1.21.9 dwz=0.14-1 file=1:5.41-4 findutils=4.9.0-3 g++=4:11.2.0-2 g++-11=11.3.0-4 gcc=4:11.2.0-2 gcc-11=11.3.0-4 gcc-11-base=11.3.0-4 gcc-12-base=12.1.0-5 gettext=0.21-6 gettext-base=0.21-6 grep=3.7-1 groff-base=1.22.4-8 gzip=1.12-1 hostname=3.23 init-system-helpers=1.63 intltool-debian=0.35.0+20060710.5 libacl1=2.3.1-1 libarchive-zip-perl=1.68-1 libasan6=11.3.0-4 libatomic1=12.1.0-5 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libbinutils=2.38.50.20220629-4 libblkid1=2.38-4 libbz2-1.0=1.0.8-5 libc-bin=2.33-7 libc-dev-bin=2.33-7 libc6=2.33-7 libc6-dev=2.33-7 libcap-ng0=0.8.3-1 libcap2=1:2.44-1 libcc1-0=12.1.0-5 libcom-err2=1.46.5-2 libcoq-core-ocaml=8.15.2+dfsg-2 libcoq-core-ocaml-dev=8.15.2+dfsg-2 libcoq-mathcomp-ssreflect=1.15.0-1 libcoq-stdlib=8.15.2+dfsg-2 libcrypt-dev=1:4.4.28-1 libcrypt1=1:4.4.28-1 libctf-nobfd0=2.38.50.20220629-4 libctf0=2.38.50.20220629-4 libdb5.3=5.3.28+dfsg1-0.10 libdebconfclient0=0.263 libdebhelper-perl=13.8 libdpkg-perl=1.21.9 libelf1=0.187-1 libexpat1=2.4.8-1 libffi8=3.4.2-4 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libgcc-11-dev=11.3.0-4 libgcc-s1=12.1.0-5 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libgmp-dev=2:6.2.1+dfsg1-1 libgmp10=2:6.2.1+dfsg1-1 libgmp3-dev=2:6.2.1+dfsg1-1 libgmpxx4ldbl=2:6.2.1+dfsg1-1 libgomp1=12.1.0-5 libgpg-error0=1.45-2 libgprofng0=2.38.50.20220629-4 libgssapi-krb5-2=1.19.2-2+b2 libicu71=71.1-3 libisl23=0.24-2 libitm1=12.1.0-5 libk5crypto3=1.19.2-2+b2 libkeyutils1=1.6.3-1 libkrb5-3=1.19.2-2+b2 libkrb5support0=1.19.2-2+b2 liblsan0=12.1.0-5 liblz4-1=1.9.3-2 liblzma5=5.2.5-2.1 libmagic-mgc=1:5.41-4 libmagic1=1:5.41-4 libmount1=2.38-4 libmpc3=1.2.1-2 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libncurses-dev=6.3+20220423-2 libncurses5-dev=6.3+20220423-2 libncurses6=6.3+20220423-2 libncursesw6=6.3+20220423-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libpam-modules=1.4.0-13 libpam-modules-bin=1.4.0-13 libpam-runtime=1.4.0-13 libpam0g=1.4.0-13 libpcre2-8-0=10.40-1 libpcre3=2:8.39-14 libperl5.34=5.34.0-4 libpipeline1=1.5.6-1 libpython3-stdlib=3.10.4-1+b1 libpython3.10-minimal=3.10.5-1 libpython3.10-stdlib=3.10.5-1 libquadmath0=12.1.0-5 libreadline8=8.1.2-1.2 libseccomp2=2.5.4-1 libselinux1=3.4-1 libsigsegv2=2.14-1 libsmartcols1=2.38-4 libsqlite3-0=3.39.0-1 libssl3=3.0.4-2 libstdc++-11-dev=11.3.0-4 libstdc++6=12.1.0-5 libsub-override-perl=0.09-3 libsystemd0=251.2-7 libtinfo6=6.3+20220423-2 libtirpc-common=1.3.2-2 libtirpc-dev=1.3.2-2 libtirpc3=1.3.2-2 libtool=2.4.7-4 libtsan0=11.3.0-4 libubsan1=12.1.0-5 libuchardet0=0.0.7-1 libudev1=251.2-7 libunistring2=1.0-1 libuuid1=2.38-4 libxml2=2.9.14+dfsg-1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.5.2+dfsg-1 linux-libc-dev=5.18.5-1 login=1:4.11.1+dfsg1-2 lsb-base=11.2 m4=1.4.18-5 make=4.3-4.1 man-db=2.10.2-1 mawk=1.3.4.20200120-3.1 media-types=8.0.0 ncurses-base=6.3+20220423-2 ncurses-bin=6.3+20220423-2 ocaml=4.13.1-3 ocaml-base=4.13.1-3 ocaml-compiler-libs=4.13.1-3 ocaml-findlib=1.9.3-1 ocaml-interp=4.13.1-3 ocaml-nox=4.13.1-3 patch=2.7.6-7 perl=5.34.0-4 perl-base=5.34.0-4 perl-modules-5.34=5.34.0-4 po-debconf=1.0.21+nmu1 python3=3.10.4-1+b1 python3-minimal=3.10.4-1+b1 python3.10=3.10.5-1 python3.10-minimal=3.10.5-1 readline-common=8.1.2-1.2 rpcsvc-proto=1.4.2-4 sed=4.8-1 sensible-utils=0.0.17 sysvinit-utils=3.03-1 tar=1.34+dfsg-1 util-linux=2.38-4 util-linux-extra=2.38-4 xz-utils=5.2.5-2.1 zlib1g=1:1.2.11.dfsg-4 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220710T025311Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220710T025311Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220804T025752Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220704T093053Z/ 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 coquelicot=3.2.0-7 && mkdir -p /build/coquelicot-n17pwX && dpkg-source --no-check -x /*.dsc /build/coquelicot-n17pwX/coquelicot-3.2.0 && chown -R builduser:builduser /build/coquelicot-n17pwX" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coquelicot-n17pwX/coquelicot-3.2.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1657005732" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/coquelicot-n17pwX /tmp/coquelicot-3.2.0-7yn9nffpe bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220704T093053Z 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._lf7kOypys 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._lf7kOypys Reading package lists... Building dependency tree... util-linux is already the newest version (2.38-4). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 136 kB of archives. After this operation, 401 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20220704T093053Z unstable/main amd64 libfakeroot amd64 1.29-1 [48.5 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220704T093053Z 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 (1002 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 ... 4627 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.29-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.29-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.29-1_amd64.deb ... Unpacking fakeroot (1.29-1) ... Setting up libfakeroot:amd64 (1.29-1) ... Setting up fakeroot (1.29-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.33-7) ... I: running special hook: copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220710T025311Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20220710T025311Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20220804T025752Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220704T093053Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap._lf7kOypys Get:1 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm InRelease [130 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220804T025752Z unstable InRelease [192 kB] Hit:3 http://snapshot.notset.fr/archive/debian/20220704T093053Z unstable InRelease Ign:4 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main amd64 Packages Get:4 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main Sources [12.1 MB] Get:5 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main amd64 Packages [11.5 MB] Ign:6 http://snapshot.notset.fr/archive/debian/20220804T025752Z unstable/main amd64 Packages Err:6 http://snapshot.notset.fr/archive/debian/20220804T025752Z unstable/main amd64 Packages 404 Not Found [IP: 10.13.0.253 80] Ign:6 http://snapshot.notset.fr/archive/debian/20220804T025752Z unstable/main amd64 Packages Get:6 http://snapshot.notset.fr/archive/debian/20220804T025752Z unstable/main amd64 Packages [12.6 MB] Fetched 36.5 MB in 30s (1230 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._lf7kOypys I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d coquelicot=3.2.0-7 && mkdir -p /build/coquelicot-n17pwX && dpkg-source --no-check -x /*.dsc /build/coquelicot-n17pwX/coquelicot-3.2.0 && chown -R builduser:builduser /build/coquelicot-n17pwX"' exec /tmp/mmdebstrap._lf7kOypys Reading package lists... NOTICE: 'coquelicot' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/coquelicot.git Please use: git clone https://salsa.debian.org/ocaml-team/coquelicot.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 282 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main coquelicot 3.2.0-7 (dsc) [2080 B] Get:2 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main coquelicot 3.2.0-7 (tar) [278 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220710T025311Z bookworm/main coquelicot 3.2.0-7 (diff) [2320 B] Fetched 282 kB in 0s (1040 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'coquelicot_3.2.0-7.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting coquelicot in /build/coquelicot-n17pwX/coquelicot-3.2.0 dpkg-source: info: unpacking coquelicot_3.2.0.orig.tar.gz dpkg-source: info: unpacking coquelicot_3.2.0-7.debian.tar.xz dpkg-source: info: using patch list from debian/patches/series dpkg-source: info: applying fix_paths.patch I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/coquelicot-n17pwX/coquelicot-3.2.0 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1657005732" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap._lf7kOypys dpkg-buildpackage: info: source package coquelicot dpkg-buildpackage: info: source version 3.2.0-7 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Julien Puydt dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with coq,ocaml dh_ocamlclean dh_clean debian/rules binary-arch dh binary-arch --with coq,ocaml 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_ocamlinit -a debian/rules override_dh_auto_configure make[1]: Entering directory '/build/coquelicot-n17pwX/coquelicot-3.2.0' autoconf configure.in:5: warning: prefer named diversions ./configure checking for coqc... /usr/bin/coqc checking for coqdep... /usr/bin/coqdep checking for coqdoc... /usr/bin/coqdoc checking for SSReflect... yes checking for g++... g++ 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 g++ accepts -g... yes checking for g++ option to enable C++11 features... none needed configure: building remake... /usr/bin/ld: /tmp/ccDvjo45.o: in function `main': remake.cpp:(.text.startup+0xbb2): warning: the use of `tempnam' is dangerous, better use `mkstemp' configure: creating ./config.status config.status: creating Remakefile make[1]: Leaving directory '/build/coquelicot-n17pwX/coquelicot-3.2.0' debian/rules override_dh_auto_build make[1]: Entering directory '/build/coquelicot-n17pwX/coquelicot-3.2.0' ./remake Building theories/AutoDerive.vo Building theories/Continuity.vo Building theories/Compactness.vo Building theories/Rcomplements.vo File "./theories/Rcomplements.v", line 660, characters 2-37: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Rcomplements.v", line 676, characters 2-20: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./theories/Rcomplements.v", line 1383, characters 2-54: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./theories/Rcomplements.v", line 1413, characters 2-54: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./theories/Rcomplements.v", line 1434, characters 2-49: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Rcomplements.v", line 1439, characters 2-26: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1637, characters 19-28: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1638, characters 24-34: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1637, characters 19-28: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1638, characters 24-34: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1637, characters 19-28: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1630, characters 2-460: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1638, characters 24-34: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1656, characters 35-48: Warning: Notation RList.Rlength is deprecated since 8.12. use List.length instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1657, characters 19-29: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1657, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1658, characters 21-31: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1658, characters 36-46: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1666, characters 35-45: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/Rcomplements.v", line 1666, characters 49-59: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] Finished theories/Rcomplements.vo Finished theories/Compactness.vo Building theories/Hierarchy.vo Building theories/Iter.vo File "./theories/Iter.v", line 187, characters 12-20: Warning: Notation iota_add is deprecated since mathcomp 1.13.0. Use iotaD instead. [deprecated-syntactic-definition,deprecated] File "./theories/Iter.v", line 187, characters 12-20: Warning: Notation iota_add is deprecated since mathcomp 1.13.0. Use iotaD instead. [deprecated-syntactic-definition,deprecated] File "./theories/Iter.v", line 187, characters 12-20: Warning: Notation iota_add is deprecated since mathcomp 1.13.0. Use iotaD instead. [deprecated-syntactic-definition,deprecated] Finished theories/Iter.vo Building theories/Lub.vo Building theories/Markov.vo Finished theories/Markov.vo Building theories/Rbar.vo File "./theories/Rbar.v", line 49, characters 0-27: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Rbar.vo File "./theories/Lub.v", line 24, characters 0-40: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Lub.vo File "./theories/Hierarchy.v", line 24, characters 0-49: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Hierarchy.v", line 1917, characters 0-47: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 1940, characters 0-77: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2169, characters 0-20: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2183, characters 0-25: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2188, characters 0-25: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2397, characters 2-41: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2422, characters 2-37: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2554, characters 2-54: Warning: Duplicate clear of HFc [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2559, characters 2-40: Warning: Duplicate clear of H0 [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2560, characters 2-47: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2561, characters 2-61: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2615, characters 2-23: Warning: Duplicate clear of Hfg [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2623, characters 2-23: Warning: Duplicate clear of Hhl [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2662, characters 2-23: Warning: Duplicate clear of Hfg [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2666, characters 2-115: Warning: Duplicate clear of Hfh [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 2675, characters 2-64: Warning: Duplicate clear of Hfh [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 4453, characters 2-36: Warning: Duplicate clear of A [duplicate-clear,ssr] File "./theories/Hierarchy.v", line 4488, characters 2-36: Warning: Duplicate clear of A [duplicate-clear,ssr] Finished theories/Hierarchy.vo Building theories/Lim_seq.vo File "./theories/Lim_seq.v", line 24, characters 0-54: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Lim_seq.v", line 268, characters 2-211: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 268, characters 2-211: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 268, characters 2-211: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 268, characters 2-211: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 280, characters 2-121: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 284, characters 2-119: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 286, characters 2-88: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 290, characters 2-91: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 303, characters 2-211: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 303, characters 2-211: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 303, characters 2-211: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 303, characters 2-211: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 317, characters 2-121: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 321, characters 2-91: Warning: Duplicate clear of Hl0 [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 323, characters 2-119: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 325, characters 2-88: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 482, characters 2-235: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 508, characters 2-166: Warning: Duplicate clear of Hiu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 508, characters 2-166: Warning: Duplicate clear of Hsu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 517, characters 2-133: Warning: Duplicate clear of Hiu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 520, characters 2-133: Warning: Duplicate clear of Hsu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 536, characters 2-60: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 726, characters 2-38: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 744, characters 2-28: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 1512, characters 2-103: Warning: Duplicate clear of Hcv [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 1517, characters 2-103: Warning: Duplicate clear of Hcv [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 2113, characters 2-31: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 2130, characters 2-31: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 2139, characters 2-31: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 2178, characters 2-38: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 2185, characters 2-38: Warning: Duplicate clear of Hu [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 2465, characters 4-58: Warning: Duplicate clear of Hl [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 2857, characters 2-43: Warning: Duplicate clear of Ha [duplicate-clear,ssr] File "./theories/Lim_seq.v", line 3155, characters 2-76: Warning: Duplicate clear of H2 [duplicate-clear,ssr] Finished theories/Lim_seq.vo File "./theories/Continuity.v", line 24, characters 0-63: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Continuity.v", line 863, characters 4-75: Warning: Duplicate clear of Cf [duplicate-clear,ssr] File "./theories/Continuity.v", line 885, characters 2-68: Warning: Duplicate clear of He [duplicate-clear,ssr] File "./theories/Continuity.v", line 1000, characters 2-46: Warning: Duplicate clear of Hab [duplicate-clear,ssr] File "./theories/Continuity.v", line 1808, characters 2-66: Warning: Duplicate clear of Cf [duplicate-clear,ssr] File "./theories/Continuity.v", line 1820, characters 4-41: Warning: Duplicate clear of eps [duplicate-clear,ssr] Finished theories/Continuity.vo Building theories/Derive.vo Building theories/Equiv.vo File "./theories/Equiv.v", line 24, characters 0-43: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Equiv.vo File "./theories/Derive.v", line 26, characters 0-73: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Derive.v", line 352, characters 2-21: Warning: Duplicate clear of Df [duplicate-clear,ssr] File "./theories/Derive.v", line 2189, characters 2-63: Warning: Duplicate clear of Cf [duplicate-clear,ssr] File "./theories/Derive.v", line 2190, characters 2-63: Warning: Duplicate clear of Cg [duplicate-clear,ssr] File "./theories/Derive.v", line 2214, characters 2-33: Warning: Duplicate clear of Cf [duplicate-clear,ssr] File "./theories/Derive.v", line 2215, characters 2-33: Warning: Duplicate clear of Cg [duplicate-clear,ssr] File "./theories/Derive.v", line 2216, characters 2-62: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/Derive.v", line 2306, characters 2-29: Warning: Duplicate clear of Hbx [duplicate-clear,ssr] File "./theories/Derive.v", line 2324, characters 2-29: Warning: Duplicate clear of Hax [duplicate-clear,ssr] File "./theories/Derive.v", line 2460, characters 2-29: Warning: Duplicate clear of Hbx [duplicate-clear,ssr] File "./theories/Derive.v", line 2491, characters 2-29: Warning: Duplicate clear of Hax [duplicate-clear,ssr] File "./theories/Derive.v", line 3308, characters 6-22: Warning: Duplicate clear of Hy [duplicate-clear,ssr] File "./theories/Derive.v", line 3387, characters 2-37: Warning: Duplicate clear of f [duplicate-clear,ssr] File "./theories/Derive.v", line 3403, characters 2-38: Warning: Duplicate clear of f [duplicate-clear,ssr] File "./theories/Derive.v", line 3420, characters 2-38: Warning: Duplicate clear of f [duplicate-clear,ssr] Finished theories/Derive.vo Building theories/Derive_2d.vo File "./theories/Derive_2d.v", line 1196, characters 2-43: Warning: Duplicate clear of z [duplicate-clear,ssr] Finished theories/Derive_2d.vo Building theories/ElemFct.vo Building theories/PSeries.vo Building theories/Seq_fct.vo Building theories/Series.vo File "./theories/Series.v", line 24, characters 0-51: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Series.v", line 967, characters 4-28: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Series.v", line 1026, characters 4-34: Warning: Duplicate clear of Hda [duplicate-clear,ssr] File "./theories/Series.v", line 1047, characters 2-16: Warning: Duplicate clear of H [duplicate-clear,ssr] Finished theories/Series.vo File "./theories/Seq_fct.v", line 23, characters 0-80: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Seq_fct.v", line 159, characters 2-59: Warning: Duplicate clear of H0 [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 180, characters 2-59: Warning: Duplicate clear of H0 [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 243, characters 4-35: Warning: Duplicate clear of Hy [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 279, characters 4-64: Warning: Duplicate clear of Hfn [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 280, characters 4-41: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 281, characters 4-36: Warning: Duplicate clear of Hex [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 316, characters 2-97: Warning: Duplicate clear of x [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 392, characters 4-36: Warning: Duplicate clear of Edn [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 702, characters 4-82: Warning: Duplicate clear of Hcvs [duplicate-clear,ssr] File "./theories/Seq_fct.v", line 714, characters 4-82: Warning: Duplicate clear of Hcvs [duplicate-clear,ssr] Finished theories/Seq_fct.vo File "./theories/PSeries.v", line 24, characters 0-88: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/PSeries.v", line 537, characters 2-59: Warning: Duplicate clear of Hnot_ex [duplicate-clear,ssr] File "./theories/PSeries.v", line 660, characters 4-44: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/PSeries.v", line 1268, characters 2-53: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/PSeries.v", line 1306, characters 2-53: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/PSeries.v", line 1474, characters 2-33: Warning: Duplicate clear of H0 [duplicate-clear,ssr] File "./theories/PSeries.v", line 1481, characters 2-26: Warning: Duplicate clear of H0 [duplicate-clear,ssr] File "./theories/PSeries.v", line 2045, characters 4-64: Warning: Duplicate clear of Hn [duplicate-clear,ssr] File "./theories/PSeries.v", line 2045, characters 4-64: Warning: Duplicate clear of Hn [duplicate-clear,ssr] File "./theories/PSeries.v", line 2441, characters 4-46: Warning: Duplicate clear of r [duplicate-clear,ssr] File "./theories/PSeries.v", line 2457, characters 3-82: Warning: Duplicate clear of Hw [duplicate-clear,ssr] Finished theories/PSeries.vo Building theories/RInt.vo Building theories/SF_seq.vo File "./theories/SF_seq.v", line 25, characters 0-47: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/SF_seq.v", line 38, characters 14-23: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 39, characters 14-24: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 41, characters 24-35: Warning: Notation RList.Rlist is deprecated since 8.12. use (list R) instead [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 41, characters 0-134: Warning: Notation RList.nil is deprecated since 8.12. use List.nil instead [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 41, characters 0-134: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 47, characters 25-36: Warning: Notation RList.Rlist is deprecated since 8.12. use (list R) instead [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 59, characters 2-15: Warning: Notation RList.Rlength is deprecated since 8.12. use List.length instead [deprecated-syntactic-definition,deprecated] File "./theories/SF_seq.v", line 116, characters 2-78: Warning: Duplicate clear of IHs [duplicate-clear,ssr] File "./theories/SF_seq.v", line 337, characters 2-18: Warning: Duplicate clear of IH [duplicate-clear,ssr] File "./theories/SF_seq.v", line 403, characters 2-38: Warning: Duplicate clear of IHst [duplicate-clear,ssr] File "./theories/SF_seq.v", line 845, characters 2-30: Warning: Duplicate clear of IH [duplicate-clear,ssr] File "./theories/SF_seq.v", line 918, characters 2-31: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/SF_seq.v", line 1032, characters 2-74: Warning: Duplicate clear of Hx' [duplicate-clear,ssr] File "./theories/SF_seq.v", line 1108, characters 2-30: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/SF_seq.v", line 1302, characters 2-149: Warning: Duplicate clear of Hdec [duplicate-clear,ssr] File "./theories/SF_seq.v", line 2104, characters 2-28: Warning: Duplicate clear of IH [duplicate-clear,ssr] File "./theories/SF_seq.v", line 2659, characters 4-242: Warning: Duplicate clear of Hw [duplicate-clear,ssr] File "./theories/SF_seq.v", line 2659, characters 4-242: Warning: Duplicate clear of Hw [duplicate-clear,ssr] File "./theories/SF_seq.v", line 2774, characters 4-242: Warning: Duplicate clear of Hw [duplicate-clear,ssr] File "./theories/SF_seq.v", line 2774, characters 4-242: Warning: Duplicate clear of Hw [duplicate-clear,ssr] Finished theories/SF_seq.vo File "./theories/RInt.v", line 25, characters 0-80: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/RInt.v", line 177, characters 2-23: Warning: Duplicate clear of Hex [duplicate-clear,ssr] File "./theories/RInt.v", line 191, characters 2-37: Warning: Duplicate clear of Hex [duplicate-clear,ssr] File "./theories/RInt.v", line 287, characters 2-23: Warning: Duplicate clear of Hex [duplicate-clear,ssr] File "./theories/RInt.v", line 357, characters 4-35: Warning: Duplicate clear of Hg [duplicate-clear,ssr] File "./theories/RInt.v", line 399, characters 2-22: Warning: Duplicate clear of Hex [duplicate-clear,ssr] File "./theories/RInt.v", line 464, characters 2-74: Warning: Duplicate clear of Hstep [duplicate-clear,ssr] File "./theories/RInt.v", line 552, characters 2-71: Warning: Duplicate clear of Heq [duplicate-clear,ssr] File "./theories/RInt.v", line 557, characters 2-60: Warning: Duplicate clear of Hstep [duplicate-clear,ssr] File "./theories/RInt.v", line 888, characters 2-22: Warning: Duplicate clear of If [duplicate-clear,ssr] File "./theories/RInt.v", line 912, characters 2-212: Warning: Duplicate clear of Hs [duplicate-clear,ssr] File "./theories/RInt.v", line 986, characters 2-97: Warning: Duplicate clear of H1 [duplicate-clear,ssr] File "./theories/RInt.v", line 987, characters 2-97: Warning: Duplicate clear of H2 [duplicate-clear,ssr] File "./theories/RInt.v", line 1805, characters 6-22: Warning: Duplicate clear of H0 [duplicate-clear,ssr] File "./theories/RInt.v", line 2928, characters 37-47: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2928, characters 53-63: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2928, characters 37-47: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2928, characters 53-63: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2929, characters 33-43: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2929, characters 49-59: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2929, characters 33-43: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2929, characters 49-59: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2977, characters 18-28: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2977, characters 18-28: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 2989, characters 2-27: Warning: Duplicate clear of H [duplicate-clear,ssr] File "./theories/RInt.v", line 3029, characters 2-44: Warning: Duplicate clear of IH [duplicate-clear,ssr] File "./theories/RInt.v", line 3315, characters 2-30: Warning: Duplicate clear of IH [duplicate-clear,ssr] File "./theories/RInt.v", line 3317, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3317, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3579, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3579, characters 50-60: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3579, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3579, characters 50-60: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3582, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3582, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3582, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3585, characters 33-43: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3585, characters 49-59: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3585, characters 33-43: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3585, characters 49-59: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3589, characters 33-43: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3589, characters 49-59: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3589, characters 33-43: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3589, characters 49-59: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3610, characters 2-51: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/RInt.v", line 3610, characters 2-51: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/RInt.v", line 3612, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3612, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3616, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3616, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3616, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3656, characters 2-55: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/RInt.v", line 3656, characters 2-55: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/RInt.v", line 3658, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3658, characters 34-44: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3662, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3662, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3662, characters 27-37: Warning: Notation RList.cons is deprecated since 8.12. use List.cons instead [deprecated-syntactic-definition,deprecated] File "./theories/RInt.v", line 3741, characters 2-107: Warning: Duplicate clear of IH [duplicate-clear,ssr] File "./theories/RInt.v", line 3797, characters 2-148: Warning: Duplicate clear of Hptd [duplicate-clear,ssr] File "./theories/RInt.v", line 3806, characters 2-159: Warning: Duplicate clear of IH [duplicate-clear,ssr] File "./theories/RInt.v", line 3896, characters 4-50: Warning: Duplicate clear of Hab [duplicate-clear,ssr] File "./theories/RInt.v", line 3896, characters 4-50: Warning: Duplicate clear of Hab [duplicate-clear,ssr] File "./theories/RInt.v", line 4015, characters 4-79: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/RInt.v", line 4286, characters 2-23: Warning: Duplicate clear of HIf [duplicate-clear,ssr] File "./theories/RInt.v", line 4301, characters 2-23: Warning: Duplicate clear of HIf [duplicate-clear,ssr] File "./theories/RInt.v", line 4324, characters 2-22: Warning: Duplicate clear of HIf [duplicate-clear,ssr] File "./theories/RInt.v", line 4386, characters 2-23: Warning: Duplicate clear of HIf [duplicate-clear,ssr] File "./theories/RInt.v", line 4446, characters 6-34: Warning: Duplicate clear of H1 [duplicate-clear,ssr] File "./theories/RInt.v", line 4446, characters 6-34: Warning: Duplicate clear of H1 [duplicate-clear,ssr] File "./theories/RInt.v", line 4481, characters 6-34: Warning: Duplicate clear of Ht [duplicate-clear,ssr] File "./theories/RInt.v", line 4481, characters 6-34: Warning: Duplicate clear of Ht [duplicate-clear,ssr] File "./theories/RInt.v", line 4495, characters 6-34: Warning: Duplicate clear of H1 [duplicate-clear,ssr] File "./theories/RInt.v", line 4495, characters 6-34: Warning: Duplicate clear of H1 [duplicate-clear,ssr] File "./theories/RInt.v", line 4584, characters 2-23: Warning: Duplicate clear of HIf [duplicate-clear,ssr] Finished theories/RInt.vo Building theories/RInt_analysis.vo File "./theories/RInt_analysis.v", line 27, characters 0-66: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/RInt_analysis.v", line 48, characters 4-104: Warning: Duplicate clear of CIf [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 113, characters 2-114: Warning: Duplicate clear of CIf [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 338, characters 2-59: Warning: Duplicate clear of Hf [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 471, characters 2-95: Warning: Duplicate clear of Ha [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 475, characters 2-95: Warning: Duplicate clear of Hb [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 693, characters 2-60: Warning: Duplicate clear of Hf [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 774, characters 0-57: Warning: Duplicate clear of Ca [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 794, characters 0-57: Warning: Duplicate clear of Ca [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 795, characters 0-57: Warning: Duplicate clear of Cb [duplicate-clear,ssr] File "./theories/RInt_analysis.v", line 1284, characters 0-58: Warning: Duplicate clear of Hy [duplicate-clear,ssr] Finished theories/RInt_analysis.vo File "./theories/ElemFct.v", line 24, characters 0-96: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/ElemFct.v", line 556, characters 2-30: Warning: Duplicate clear of Hy [duplicate-clear,ssr] File "./theories/ElemFct.v", line 570, characters 2-36: Warning: Duplicate clear of n [duplicate-clear,ssr] File "./theories/ElemFct.v", line 666, characters 2-56: Warning: Duplicate clear of Hx [duplicate-clear,ssr] File "./theories/ElemFct.v", line 674, characters 2-53: Warning: Duplicate clear of n [duplicate-clear,ssr] Finished theories/ElemFct.vo File "./theories/AutoDerive.v", line 763, characters 0-65: Warning: Duplicate clear of Dle [duplicate-clear,ssr] File "./theories/AutoDerive.v", line 961, characters 0-45: Warning: Duplicate clear of IHe1 [duplicate-clear,ssr] Finished theories/AutoDerive.vo Building theories/Complex.vo File "./theories/Complex.v", line 24, characters 0-61: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] File "./theories/Complex.v", line 71, characters 0-29: Warning: Declaring a scope implicitly is deprecated; use in advance an explicit "Declare Scope C_scope.". [undeclared-scope,deprecated] File "./theories/Complex.v", line 507, characters 0-135: Warning: Ignoring canonical projection to C by ModuleSpace.sort in C_R_ModuleSpace: redundant with C_ModuleSpace [redundant-canonical-projection,typechecker] File "./theories/Complex.v", line 510, characters 0-167: Warning: Ignoring canonical projection to C by NormedModuleAux.sort in C_R_NormedModuleAux: redundant with C_NormedModuleAux [redundant-canonical-projection,typechecker] File "./theories/Complex.v", line 513, characters 0-113: Warning: Ignoring canonical projection to C by NormedModule.sort in C_R_NormedModule: redundant with C_NormedModule [redundant-canonical-projection,typechecker] File "./theories/Complex.v", line 590, characters 0-175: Warning: Ignoring canonical projection to C by CompleteNormedModule.sort in C_R_CompleteNormedModule: redundant with C_CompleteNormedModule [redundant-canonical-projection,typechecker] Finished theories/Complex.vo Building theories/Coquelicot.vo Building theories/RInt_gen.vo File "./theories/RInt_gen.v", line 24, characters 0-88: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/RInt_gen.vo File "./theories/Coquelicot.v", line 272, characters 0-52: Warning: New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function. [ambiguous-paths,typechecker] Finished theories/Coquelicot.vo Building theories/KHInt.vo Finished theories/KHInt.vo Building all Finished all make[1]: Leaving directory '/build/coquelicot-n17pwX/coquelicot-3.2.0' create-stamp debian/debhelper-build-stamp dh_prep -a dh_auto_install --destdir=debian/libcoq-coquelicot/ -a dh_install -a dh_ocamldoc -a dh_installdocs -a debian/rules override_dh_installchangelogs make[1]: Entering directory '/build/coquelicot-n17pwX/coquelicot-3.2.0' dh_installchangelogs NEWS.md make[1]: Leaving directory '/build/coquelicot-n17pwX/coquelicot-3.2.0' dh_installexamples -a dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a dh_missing -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_coq -a dh_ocaml -a dh_gencontrol -a dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libcoq-coquelicot' in '../libcoq-coquelicot_3.2.0-7_amd64.deb'. dpkg-genbuildinfo --build=any -O../coquelicot_3.2.0-7_amd64.buildinfo dpkg-genchanges --build=any -O../coquelicot_3.2.0-7_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/coquelicot-n17pwX /tmp/coquelicot-3.2.0-7yn9nffpe I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap._lf7kOypys... I: success in 685.7572 seconds md5: Value of 'md5' differs for libcoq-coquelicot_3.2.0-7_amd64.deb sha1: Value of 'sha1' differs for libcoq-coquelicot_3.2.0-7_amd64.deb sha256: Value of 'sha256' differs for libcoq-coquelicot_3.2.0-7_amd64.deb Checksums: FAIL Cannot generate diffoscope for libcoq-coquelicot_3.2.0-7_amd64.deb: RetryError[]