https://launchpad.net/ubuntu/+source/mathcomp-real-closed/1.1.4-2build1/+build/26962135 RUN: /usr/share/launchpad-buildd/bin/builder-prep Kernel version: Linux riscv64-qemu-lgw01-082 5.13.0-1019-generic #21~20.04.1-Ubuntu SMP Thu Mar 24 22:36:01 UTC 2022 riscv64 Buildd toolchain package versions: launchpad-buildd_234~642~ubuntu20.04.1 python3-lpbuildd_234~642~ubuntu20.04.1 sbuild_0.79.0-1ubuntu1 git_1:2.25.1-1ubuntu3.2 dpkg-dev_1.19.7ubuntu3.2 python3-debian_0.1.36ubuntu1. Syncing the system clock with the buildd NTP service... 16 Nov 01:55:16 ntpdate[3763247]: adjust time server 10.211.37.1 offset -0.001908 sec RUN: /usr/share/launchpad-buildd/bin/in-target unpack-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962135 --image-type chroot /home/buildd/filecache-default/20a3246b7a16d5658607d7f37229fcda30a33651 Creating target for build PACKAGEBUILD-26962135 RUN: /usr/share/launchpad-buildd/bin/in-target mount-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962135 Starting target for build PACKAGEBUILD-26962135 RUN: /usr/share/launchpad-buildd/bin/in-target override-sources-list --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962135 'deb http://ftpmaster.internal/ubuntu noble main universe' 'deb http://ftpmaster.internal/ubuntu noble-security main universe' 'deb http://ftpmaster.internal/ubuntu noble-updates main universe' 'deb http://ftpmaster.internal/ubuntu noble-proposed main universe' Overriding sources.list in build-PACKAGEBUILD-26962135 RUN: /usr/share/launchpad-buildd/bin/in-target update-debian-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962135 Updating target for build PACKAGEBUILD-26962135 Get:1 http://ftpmaster.internal/ubuntu noble InRelease [240 kB] Get:2 http://ftpmaster.internal/ubuntu noble-security InRelease [74.9 kB] Get:3 http://ftpmaster.internal/ubuntu noble-updates InRelease [74.9 kB] Get:4 http://ftpmaster.internal/ubuntu noble-proposed InRelease [102 kB] Get:5 http://ftpmaster.internal/ubuntu noble/main riscv64 Packages [1341 kB] Get:6 http://ftpmaster.internal/ubuntu noble/main Translation-en [517 kB] Get:7 http://ftpmaster.internal/ubuntu noble/universe riscv64 Packages [14.3 MB] Get:8 http://ftpmaster.internal/ubuntu noble/universe Translation-en [6012 kB] Get:9 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 Packages [82.3 kB] Get:10 http://ftpmaster.internal/ubuntu noble-proposed/main Translation-en [34.2 kB] Get:11 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 Packages [1398 kB] Get:12 http://ftpmaster.internal/ubuntu noble-proposed/universe Translation-en [446 kB] Fetched 24.6 MB in 30s (830 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... Calculating upgrade... The following package was automatically installed and is no longer required: libunistring2 Use 'sudo apt autoremove' to remove it. The following NEW packages will be installed: libunistring5 The following packages will be upgraded: apt apt-utils base-files base-passwd bash bash-completion binutils binutils-common binutils-riscv64-linux-gnu cpp-13 debianutils diffutils dpkg dpkg-dev fakeroot g++-13 gcc-13 gcc-13-base grep libapparmor1 libapt-pkg6.0 libargon2-1 libasan8 libatomic1 libaudit-common libaudit1 libbinutils libc-bin libc-dev-bin libc6 libc6-dev libcap-ng0 libcc1-0 libctf-nobfd0 libctf0 libdb5.3 libdpkg-perl libfakeroot libgcc-13-dev libgcc-s1 libgnutls30 libgomp1 libidn2-0 liblzma5 libncursesw6 libnsl-dev libnsl2 libpng16-16 libseccomp2 libselinux1 libsemanage-common libsemanage2 libsframe1 libsqlite3-0 libssl3 libstdc++-13-dev libstdc++6 libsystemd-shared libsystemd0 libtinfo6 libtirpc-common libtirpc-dev libtirpc3 libudev1 libxxhash0 libzstd1 mawk ncurses-base ncurses-bin openssl optipng systemd systemd-dev systemd-sysv xz-utils 75 upgraded, 1 newly installed, 0 to remove and 0 not upgraded. Need to get 85.2 MB of archives. After this operation, 2616 kB of additional disk space will be used. Get:1 http://ftpmaster.internal/ubuntu noble/main riscv64 libnsl-dev riscv64 1.3.0-3 [135 kB] Get:2 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc6-dev riscv64 2.38-3ubuntu1 [3401 kB] Get:3 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc-dev-bin riscv64 2.38-3ubuntu1 [19.2 kB] Get:4 http://ftpmaster.internal/ubuntu noble/main riscv64 libtirpc-common all 1.3.4+ds-1 [7920 B] Get:5 http://ftpmaster.internal/ubuntu noble/main riscv64 libtirpc-dev riscv64 1.3.4+ds-1 [344 kB] Get:6 http://ftpmaster.internal/ubuntu noble/main riscv64 libtirpc3 riscv64 1.3.4+ds-1 [88.4 kB] Get:7 http://ftpmaster.internal/ubuntu noble/main riscv64 libnsl2 riscv64 1.3.0-3 [42.0 kB] Get:8 http://ftpmaster.internal/ubuntu noble/main riscv64 libcc1-0 riscv64 13.2.0-6ubuntu1 [45.4 kB] Get:9 http://ftpmaster.internal/ubuntu noble/main riscv64 gcc-13-base riscv64 13.2.0-6ubuntu1 [44.3 kB] Get:10 http://ftpmaster.internal/ubuntu noble/main riscv64 libgcc-s1 riscv64 13.2.0-6ubuntu1 [57.1 kB] Get:11 http://ftpmaster.internal/ubuntu noble/main riscv64 libgomp1 riscv64 13.2.0-6ubuntu1 [140 kB] Get:12 http://ftpmaster.internal/ubuntu noble/main riscv64 libatomic1 riscv64 13.2.0-6ubuntu1 [9488 B] Get:13 http://ftpmaster.internal/ubuntu noble/main riscv64 libasan8 riscv64 13.2.0-6ubuntu1 [2509 kB] Get:14 http://ftpmaster.internal/ubuntu noble/main riscv64 g++-13 riscv64 13.2.0-6ubuntu1 [11.9 MB] Get:15 http://ftpmaster.internal/ubuntu noble/main riscv64 libstdc++-13-dev riscv64 13.2.0-6ubuntu1 [5449 kB] Get:16 http://ftpmaster.internal/ubuntu noble/main riscv64 libgcc-13-dev riscv64 13.2.0-6ubuntu1 [3123 kB] Get:17 http://ftpmaster.internal/ubuntu noble/main riscv64 gcc-13 riscv64 13.2.0-6ubuntu1 [20.8 MB] Get:18 http://ftpmaster.internal/ubuntu noble/main riscv64 cpp-13 riscv64 13.2.0-6ubuntu1 [10.5 MB] Get:19 http://ftpmaster.internal/ubuntu noble/main riscv64 libstdc++6 riscv64 13.2.0-6ubuntu1 [779 kB] Get:20 http://ftpmaster.internal/ubuntu noble/main riscv64 libzstd1 riscv64 1.5.5+dfsg2-2 [349 kB] Get:21 http://ftpmaster.internal/ubuntu noble/main riscv64 libctf0 riscv64 2.41-6ubuntu1 [103 kB] Get:22 http://ftpmaster.internal/ubuntu noble/main riscv64 libctf-nobfd0 riscv64 2.41-6ubuntu1 [105 kB] Get:23 http://ftpmaster.internal/ubuntu noble/main riscv64 libsframe1 riscv64 2.41-6ubuntu1 [15.6 kB] Get:24 http://ftpmaster.internal/ubuntu noble/main riscv64 libbinutils riscv64 2.41-6ubuntu1 [483 kB] Get:25 http://ftpmaster.internal/ubuntu noble/main riscv64 binutils-common riscv64 2.41-6ubuntu1 [221 kB] Get:26 http://ftpmaster.internal/ubuntu noble/main riscv64 binutils riscv64 2.41-6ubuntu1 [2996 B] Get:27 http://ftpmaster.internal/ubuntu noble/main riscv64 binutils-riscv64-linux-gnu riscv64 2.41-6ubuntu1 [894 kB] Get:28 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc6 riscv64 2.38-3ubuntu1 [2742 kB] Get:29 http://ftpmaster.internal/ubuntu noble/main riscv64 base-files riscv64 13ubuntu4 [73.5 kB] Get:30 http://ftpmaster.internal/ubuntu noble/main riscv64 debianutils riscv64 5.14 [88.8 kB] Get:31 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 bash riscv64 5.2.15-2ubuntu2 [745 kB] Get:32 http://ftpmaster.internal/ubuntu noble/main riscv64 diffutils riscv64 1:3.10-1 [180 kB] Get:33 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 liblzma5 riscv64 5.4.4-0.1 [127 kB] Get:34 http://ftpmaster.internal/ubuntu noble/main riscv64 libapparmor1 riscv64 4.0.0~alpha2-0ubuntu6 [48.2 kB] Get:35 http://ftpmaster.internal/ubuntu noble/main riscv64 libaudit-common all 1:3.1.1-1build1 [5510 B] Get:36 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libcap-ng0 riscv64 0.8.3-1build3 [15.3 kB] Get:37 http://ftpmaster.internal/ubuntu noble/main riscv64 libaudit1 riscv64 1:3.1.1-1build1 [47.1 kB] Get:38 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libseccomp2 riscv64 2.5.4-2ubuntu1 [51.5 kB] Get:39 http://ftpmaster.internal/ubuntu noble/main riscv64 libselinux1 riscv64 3.5-1build1 [83.1 kB] Get:40 http://ftpmaster.internal/ubuntu noble/main riscv64 libssl3 riscv64 3.0.10-1ubuntu2.1 [1712 kB] Get:41 http://ftpmaster.internal/ubuntu noble/main riscv64 systemd-sysv riscv64 253.5-1ubuntu7 [11.5 kB] Get:42 http://ftpmaster.internal/ubuntu noble/main riscv64 systemd-dev all 253.5-1ubuntu7 [78.5 kB] Get:43 http://ftpmaster.internal/ubuntu noble/main riscv64 systemd riscv64 253.5-1ubuntu7 [3067 kB] Get:44 http://ftpmaster.internal/ubuntu noble/main riscv64 libsystemd-shared riscv64 253.5-1ubuntu7 [1903 kB] Get:45 http://ftpmaster.internal/ubuntu noble/main riscv64 libsystemd0 riscv64 253.5-1ubuntu7 [423 kB] Get:46 http://ftpmaster.internal/ubuntu noble/main riscv64 libudev1 riscv64 253.5-1ubuntu7 [163 kB] Get:47 http://ftpmaster.internal/ubuntu noble/main riscv64 libxxhash0 riscv64 0.8.2-2 [43.7 kB] Get:48 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libapt-pkg6.0 riscv64 2.7.6 [989 kB] Get:49 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 dpkg riscv64 1.22.1ubuntu2 [1394 kB] Get:50 http://ftpmaster.internal/ubuntu noble/main riscv64 grep riscv64 3.11-3 [167 kB] Get:51 http://ftpmaster.internal/ubuntu noble/main riscv64 ncurses-bin riscv64 6.4+20231016-1 [184 kB] Get:52 http://ftpmaster.internal/ubuntu noble/main riscv64 base-passwd riscv64 3.6.2 [52.1 kB] Get:53 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libc-bin riscv64 2.38-3ubuntu1 [601 kB] Get:54 http://ftpmaster.internal/ubuntu noble/main riscv64 ncurses-base all 6.4+20231016-1 [24.7 kB] Get:55 http://ftpmaster.internal/ubuntu noble/main riscv64 libdb5.3 riscv64 5.3.28+dfsg2-4 [783 kB] Get:56 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 apt riscv64 2.7.6 [1335 kB] Get:57 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 apt-utils riscv64 2.7.6 [225 kB] Get:58 http://ftpmaster.internal/ubuntu noble/main riscv64 libunistring5 riscv64 1.1-2 [544 kB] Get:59 http://ftpmaster.internal/ubuntu noble/main riscv64 libidn2-0 riscv64 2.3.4-1build1 [99.3 kB] Get:60 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libgnutls30 riscv64 3.8.1-4ubuntu3 [995 kB] Get:61 http://ftpmaster.internal/ubuntu noble/main riscv64 libsemanage-common all 3.5-1build1 [9982 B] Get:62 http://ftpmaster.internal/ubuntu noble/main riscv64 libsemanage2 riscv64 3.5-1build1 [97.7 kB] Get:63 http://ftpmaster.internal/ubuntu noble/main riscv64 libncursesw6 riscv64 6.4+20231016-1 [150 kB] Get:64 http://ftpmaster.internal/ubuntu noble/main riscv64 libtinfo6 riscv64 6.4+20231016-1 [107 kB] Get:65 http://ftpmaster.internal/ubuntu noble/main riscv64 mawk riscv64 1.3.4.20231102-1 [126 kB] Get:66 http://ftpmaster.internal/ubuntu noble/main riscv64 libargon2-1 riscv64 0~20190702+dfsg-4 [23.7 kB] Get:67 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libsqlite3-0 riscv64 3.44.0-1 [689 kB] Get:68 http://ftpmaster.internal/ubuntu noble/main riscv64 openssl riscv64 3.0.10-1ubuntu2.1 [1170 kB] Get:69 http://ftpmaster.internal/ubuntu noble/main riscv64 bash-completion all 1:2.11-8 [180 kB] Get:70 http://ftpmaster.internal/ubuntu noble/main riscv64 libpng16-16 riscv64 1.6.40-2 [189 kB] Get:71 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 xz-utils riscv64 5.4.4-0.1 [268 kB] Get:72 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 dpkg-dev all 1.22.1ubuntu2 [1148 kB] Get:73 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libdpkg-perl all 1.22.1ubuntu2 [285 kB] Get:74 http://ftpmaster.internal/ubuntu noble/main riscv64 libfakeroot riscv64 1.32.2-1 [33.3 kB] Get:75 http://ftpmaster.internal/ubuntu noble/main riscv64 fakeroot riscv64 1.32.2-1 [77.8 kB] Get:76 http://ftpmaster.internal/ubuntu noble/main riscv64 optipng riscv64 0.7.7-3 [86.9 kB] Preconfiguring packages ... Fetched 85.2 MB in 16s (5264 kB/s) (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../0-libnsl-dev_1.3.0-3_riscv64.deb ... Unpacking libnsl-dev:riscv64 (1.3.0-3) over (1.3.0-2build2) ... Preparing to unpack .../1-libc6-dev_2.38-3ubuntu1_riscv64.deb ... Unpacking libc6-dev:riscv64 (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Preparing to unpack .../2-libc-dev-bin_2.38-3ubuntu1_riscv64.deb ... Unpacking libc-dev-bin (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Preparing to unpack .../3-libtirpc-common_1.3.4+ds-1_all.deb ... Unpacking libtirpc-common (1.3.4+ds-1) over (1.3.3+ds-1) ... Preparing to unpack .../4-libtirpc-dev_1.3.4+ds-1_riscv64.deb ... Unpacking libtirpc-dev:riscv64 (1.3.4+ds-1) over (1.3.3+ds-1) ... Preparing to unpack .../5-libtirpc3_1.3.4+ds-1_riscv64.deb ... Unpacking libtirpc3:riscv64 (1.3.4+ds-1) over (1.3.3+ds-1) ... Preparing to unpack .../6-libnsl2_1.3.0-3_riscv64.deb ... Unpacking libnsl2:riscv64 (1.3.0-3) over (1.3.0-2build2) ... Preparing to unpack .../7-libcc1-0_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libcc1-0:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../8-gcc-13-base_13.2.0-6ubuntu1_riscv64.deb ... Unpacking gcc-13-base:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Setting up gcc-13-base:riscv64 (13.2.0-6ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../libgcc-s1_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libgcc-s1:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Setting up libgcc-s1:riscv64 (13.2.0-6ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../0-libgomp1_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libgomp1:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../1-libatomic1_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libatomic1:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../2-libasan8_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libasan8:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../3-g++-13_13.2.0-6ubuntu1_riscv64.deb ... Unpacking g++-13 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../4-libstdc++-13-dev_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libstdc++-13-dev:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../5-libgcc-13-dev_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libgcc-13-dev:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../6-gcc-13_13.2.0-6ubuntu1_riscv64.deb ... Unpacking gcc-13 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../7-cpp-13_13.2.0-6ubuntu1_riscv64.deb ... Unpacking cpp-13 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Preparing to unpack .../8-libstdc++6_13.2.0-6ubuntu1_riscv64.deb ... Unpacking libstdc++6:riscv64 (13.2.0-6ubuntu1) over (13.2.0-4ubuntu3) ... Setting up libstdc++6:riscv64 (13.2.0-6ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../libzstd1_1.5.5+dfsg2-2_riscv64.deb ... Unpacking libzstd1:riscv64 (1.5.5+dfsg2-2) over (1.5.5+dfsg2-1ubuntu2) ... Setting up libzstd1:riscv64 (1.5.5+dfsg2-2) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../0-libctf0_2.41-6ubuntu1_riscv64.deb ... Unpacking libctf0:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../1-libctf-nobfd0_2.41-6ubuntu1_riscv64.deb ... Unpacking libctf-nobfd0:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../2-libsframe1_2.41-6ubuntu1_riscv64.deb ... Unpacking libsframe1:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../3-libbinutils_2.41-6ubuntu1_riscv64.deb ... Unpacking libbinutils:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../4-binutils-common_2.41-6ubuntu1_riscv64.deb ... Unpacking binutils-common:riscv64 (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../5-binutils_2.41-6ubuntu1_riscv64.deb ... Unpacking binutils (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../6-binutils-riscv64-linux-gnu_2.41-6ubuntu1_riscv64.deb ... Unpacking binutils-riscv64-linux-gnu (2.41-6ubuntu1) over (2.41-5ubuntu1) ... Preparing to unpack .../7-libc6_2.38-3ubuntu1_riscv64.deb ... Unpacking libc6:riscv64 (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Setting up libc6:riscv64 (2.38-3ubuntu1) ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../base-files_13ubuntu4_riscv64.deb ... Unpacking base-files (13ubuntu4) over (13ubuntu3) ... Setting up base-files (13ubuntu4) ... Installing new version of config file /etc/issue ... Installing new version of config file /etc/issue.net ... Installing new version of config file /etc/lsb-release ... (Reading database ... 13552 files and directories currently installed.) Preparing to unpack .../debianutils_5.14_riscv64.deb ... Unpacking debianutils (5.14) over (5.8-1) ... Setting up debianutils (5.14) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../bash_5.2.15-2ubuntu2_riscv64.deb ... Unpacking bash (5.2.15-2ubuntu2) over (5.2.15-2ubuntu1) ... Setting up bash (5.2.15-2ubuntu2) ... update-alternatives: using /usr/share/man/man7/bash-builtins.7.gz to provide /usr/share/man/man7/builtins.7.gz (builtins.7.gz) in auto mode (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../diffutils_1%3a3.10-1_riscv64.deb ... Unpacking diffutils (1:3.10-1) over (1:3.8-4) ... Setting up diffutils (1:3.10-1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../liblzma5_5.4.4-0.1_riscv64.deb ... Unpacking liblzma5:riscv64 (5.4.4-0.1) over (5.4.1-0.2) ... Setting up liblzma5:riscv64 (5.4.4-0.1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libapparmor1_4.0.0~alpha2-0ubuntu6_riscv64.deb ... Unpacking libapparmor1:riscv64 (4.0.0~alpha2-0ubuntu6) over (4.0.0~alpha2-0ubuntu5) ... Preparing to unpack .../libaudit-common_1%3a3.1.1-1build1_all.deb ... Unpacking libaudit-common (1:3.1.1-1build1) over (1:3.1.1-1) ... Setting up libaudit-common (1:3.1.1-1build1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libcap-ng0_0.8.3-1build3_riscv64.deb ... Unpacking libcap-ng0:riscv64 (0.8.3-1build3) over (0.8.3-1build2) ... Setting up libcap-ng0:riscv64 (0.8.3-1build3) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libaudit1_1%3a3.1.1-1build1_riscv64.deb ... Unpacking libaudit1:riscv64 (1:3.1.1-1build1) over (1:3.1.1-1) ... Setting up libaudit1:riscv64 (1:3.1.1-1build1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libseccomp2_2.5.4-2ubuntu1_riscv64.deb ... Unpacking libseccomp2:riscv64 (2.5.4-2ubuntu1) over (2.5.4-1ubuntu3) ... Preparing to unpack .../libselinux1_3.5-1build1_riscv64.deb ... Unpacking libselinux1:riscv64 (3.5-1build1) over (3.5-1) ... Setting up libselinux1:riscv64 (3.5-1build1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libssl3_3.0.10-1ubuntu2.1_riscv64.deb ... Unpacking libssl3:riscv64 (3.0.10-1ubuntu2.1) over (3.0.10-1ubuntu2) ... Preparing to unpack .../systemd-sysv_253.5-1ubuntu7_riscv64.deb ... Unpacking systemd-sysv (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Preparing to unpack .../systemd-dev_253.5-1ubuntu7_all.deb ... Unpacking systemd-dev (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Setting up libssl3:riscv64 (3.0.10-1ubuntu2.1) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../systemd_253.5-1ubuntu7_riscv64.deb ... Unpacking systemd (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Preparing to unpack .../libsystemd-shared_253.5-1ubuntu7_riscv64.deb ... Unpacking libsystemd-shared:riscv64 (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Preparing to unpack .../libsystemd0_253.5-1ubuntu7_riscv64.deb ... Unpacking libsystemd0:riscv64 (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Setting up libsystemd0:riscv64 (253.5-1ubuntu7) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libudev1_253.5-1ubuntu7_riscv64.deb ... Unpacking libudev1:riscv64 (253.5-1ubuntu7) over (253.5-1ubuntu6) ... Setting up libudev1:riscv64 (253.5-1ubuntu7) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libxxhash0_0.8.2-2_riscv64.deb ... Unpacking libxxhash0:riscv64 (0.8.2-2) over (0.8.1-1) ... Setting up libxxhash0:riscv64 (0.8.2-2) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../libapt-pkg6.0_2.7.6_riscv64.deb ... Unpacking libapt-pkg6.0:riscv64 (2.7.6) over (2.7.3) ... Setting up libapt-pkg6.0:riscv64 (2.7.6) ... (Reading database ... 13551 files and directories currently installed.) Preparing to unpack .../dpkg_1.22.1ubuntu2_riscv64.deb ... Unpacking dpkg (1.22.1ubuntu2) over (1.22.0ubuntu1) ... Setting up dpkg (1.22.1ubuntu2) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../grep_3.11-3_riscv64.deb ... Unpacking grep (3.11-3) over (3.11-2) ... Setting up grep (3.11-3) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../ncurses-bin_6.4+20231016-1_riscv64.deb ... Unpacking ncurses-bin (6.4+20231016-1) over (6.4+20230625-2) ... Setting up ncurses-bin (6.4+20231016-1) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../base-passwd_3.6.2_riscv64.deb ... Unpacking base-passwd (3.6.2) over (3.6.1) ... Setting up base-passwd (3.6.2) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../libc-bin_2.38-3ubuntu1_riscv64.deb ... Unpacking libc-bin (2.38-3ubuntu1) over (2.38-1ubuntu6) ... Setting up libc-bin (2.38-3ubuntu1) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../ncurses-base_6.4+20231016-1_all.deb ... Unpacking ncurses-base (6.4+20231016-1) over (6.4+20230625-2) ... Setting up ncurses-base (6.4+20231016-1) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../libdb5.3_5.3.28+dfsg2-4_riscv64.deb ... Unpacking libdb5.3:riscv64 (5.3.28+dfsg2-4) over (5.3.28+dfsg2-2) ... Setting up libdb5.3:riscv64 (5.3.28+dfsg2-4) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../archives/apt_2.7.6_riscv64.deb ... Unpacking apt (2.7.6) over (2.7.3) ... Setting up apt (2.7.6) ... (Reading database ... 13549 files and directories currently installed.) Preparing to unpack .../apt-utils_2.7.6_riscv64.deb ... Unpacking apt-utils (2.7.6) over (2.7.3) ... Selecting previously unselected package libunistring5:riscv64. Preparing to unpack .../libunistring5_1.1-2_riscv64.deb ... Unpacking libunistring5:riscv64 (1.1-2) ... Setting up libunistring5:riscv64 (1.1-2) ... (Reading database ... 13554 files and directories currently installed.) Preparing to unpack .../libidn2-0_2.3.4-1build1_riscv64.deb ... Unpacking libidn2-0:riscv64 (2.3.4-1build1) over (2.3.4-1) ... Setting up libidn2-0:riscv64 (2.3.4-1build1) ... (Reading database ... 13554 files and directories currently installed.) Preparing to unpack .../libgnutls30_3.8.1-4ubuntu3_riscv64.deb ... Unpacking libgnutls30:riscv64 (3.8.1-4ubuntu3) over (3.8.1-4ubuntu1) ... Setting up libgnutls30:riscv64 (3.8.1-4ubuntu3) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../libsemanage-common_3.5-1build1_all.deb ... Unpacking libsemanage-common (3.5-1build1) over (3.5-1) ... Setting up libsemanage-common (3.5-1build1) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../libsemanage2_3.5-1build1_riscv64.deb ... Unpacking libsemanage2:riscv64 (3.5-1build1) over (3.5-1) ... Setting up libsemanage2:riscv64 (3.5-1build1) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../libncursesw6_6.4+20231016-1_riscv64.deb ... Unpacking libncursesw6:riscv64 (6.4+20231016-1) over (6.4+20230625-2) ... Preparing to unpack .../libtinfo6_6.4+20231016-1_riscv64.deb ... Unpacking libtinfo6:riscv64 (6.4+20231016-1) over (6.4+20230625-2) ... Setting up libtinfo6:riscv64 (6.4+20231016-1) ... (Reading database ... 13555 files and directories currently installed.) Preparing to unpack .../00-mawk_1.3.4.20231102-1_riscv64.deb ... Unpacking mawk (1.3.4.20231102-1) over (1.3.4.20230730-1) ... Preparing to unpack .../01-libargon2-1_0~20190702+dfsg-4_riscv64.deb ... Unpacking libargon2-1:riscv64 (0~20190702+dfsg-4) over (0~20190702+dfsg-3) ... Preparing to unpack .../02-libsqlite3-0_3.44.0-1_riscv64.deb ... Unpacking libsqlite3-0:riscv64 (3.44.0-1) over (3.42.0-1) ... Preparing to unpack .../03-openssl_3.0.10-1ubuntu2.1_riscv64.deb ... Unpacking openssl (3.0.10-1ubuntu2.1) over (3.0.10-1ubuntu2) ... Preparing to unpack .../04-bash-completion_1%3a2.11-8_all.deb ... Unpacking bash-completion (1:2.11-8) over (1:2.11-7) ... Preparing to unpack .../05-libpng16-16_1.6.40-2_riscv64.deb ... Unpacking libpng16-16:riscv64 (1.6.40-2) over (1.6.40-1) ... Preparing to unpack .../06-xz-utils_5.4.4-0.1_riscv64.deb ... Unpacking xz-utils (5.4.4-0.1) over (5.4.1-0.2) ... Preparing to unpack .../07-dpkg-dev_1.22.1ubuntu2_all.deb ... Unpacking dpkg-dev (1.22.1ubuntu2) over (1.22.0ubuntu1) ... Preparing to unpack .../08-libdpkg-perl_1.22.1ubuntu2_all.deb ... Unpacking libdpkg-perl (1.22.1ubuntu2) over (1.22.0ubuntu1) ... Preparing to unpack .../09-libfakeroot_1.32.2-1_riscv64.deb ... Unpacking libfakeroot:riscv64 (1.32.2-1) over (1.32.1-1) ... Preparing to unpack .../10-fakeroot_1.32.2-1_riscv64.deb ... Unpacking fakeroot (1.32.2-1) over (1.32.1-1) ... Preparing to unpack .../11-optipng_0.7.7-3_riscv64.deb ... Unpacking optipng (0.7.7-3) over (0.7.7-2build1) ... Setting up libapparmor1:riscv64 (4.0.0~alpha2-0ubuntu6) ... Setting up apt-utils (2.7.6) ... Setting up cpp-13 (13.2.0-6ubuntu1) ... Setting up libtirpc-common (1.3.4+ds-1) ... Setting up libargon2-1:riscv64 (0~20190702+dfsg-4) ... Setting up libsqlite3-0:riscv64 (3.44.0-1) ... Setting up binutils-common:riscv64 (2.41-6ubuntu1) ... Setting up libctf-nobfd0:riscv64 (2.41-6ubuntu1) ... Setting up systemd-dev (253.5-1ubuntu7) ... Setting up libgomp1:riscv64 (13.2.0-6ubuntu1) ... Setting up libseccomp2:riscv64 (2.5.4-2ubuntu1) ... Setting up libsframe1:riscv64 (2.41-6ubuntu1) ... Setting up libfakeroot:riscv64 (1.32.2-1) ... Setting up fakeroot (1.32.2-1) ... Setting up bash-completion (1:2.11-8) ... Setting up xz-utils (5.4.4-0.1) ... Setting up libpng16-16:riscv64 (1.6.40-2) ... Setting up libatomic1:riscv64 (13.2.0-6ubuntu1) ... Setting up libsystemd-shared:riscv64 (253.5-1ubuntu7) ... Setting up libncursesw6:riscv64 (6.4+20231016-1) ... Setting up libdpkg-perl (1.22.1ubuntu2) ... Setting up libasan8:riscv64 (13.2.0-6ubuntu1) ... Setting up mawk (1.3.4.20231102-1) ... Setting up libbinutils:riscv64 (2.41-6ubuntu1) ... Setting up libc-dev-bin (2.38-3ubuntu1) ... Setting up openssl (3.0.10-1ubuntu2.1) ... Setting up libcc1-0:riscv64 (13.2.0-6ubuntu1) ... Setting up libctf0:riscv64 (2.41-6ubuntu1) ... Setting up libtirpc3:riscv64 (1.3.4+ds-1) ... Setting up binutils-riscv64-linux-gnu (2.41-6ubuntu1) ... Setting up systemd (253.5-1ubuntu7) ... Initializing machine ID from random generator. Setting up binutils (2.41-6ubuntu1) ... Setting up dpkg-dev (1.22.1ubuntu2) ... Setting up libtirpc-dev:riscv64 (1.3.4+ds-1) ... Setting up optipng (0.7.7-3) ... Setting up libgcc-13-dev:riscv64 (13.2.0-6ubuntu1) ... Setting up libnsl2:riscv64 (1.3.0-3) ... Setting up systemd-sysv (253.5-1ubuntu7) ... Setting up gcc-13 (13.2.0-6ubuntu1) ... Setting up libnsl-dev:riscv64 (1.3.0-3) ... Setting up libc6-dev:riscv64 (2.38-3ubuntu1) ... Setting up libstdc++-13-dev:riscv64 (13.2.0-6ubuntu1) ... Setting up g++-13 (13.2.0-6ubuntu1) ... Processing triggers for debianutils (5.14) ... Processing triggers for libc-bin (2.38-3ubuntu1) ... RUN: /usr/share/launchpad-buildd/bin/sbuild-package PACKAGEBUILD-26962135 riscv64 noble-proposed -c chroot:build-PACKAGEBUILD-26962135 --arch=riscv64 --dist=noble-proposed --nolog mathcomp-real-closed_1.1.4-2build1.dsc Initiating build PACKAGEBUILD-26962135 with 8 jobs across 8 processor cores. Kernel reported to sbuild: 5.13.0-1019-generic #21~20.04.1-Ubuntu SMP Thu Mar 24 22:36:01 UTC 2022 riscv64 sbuild (Debian sbuild) 0.79.0 (05 February 2020) on riscv64-qemu-lgw01-082.buildd +==============================================================================+ | mathcomp-real-closed 1.1.4-2build1 (riscv64) Thu, 16 Nov 2023 02:02:07 +0000 | +==============================================================================+ Package: mathcomp-real-closed Version: 1.1.4-2build1 Source Version: 1.1.4-2build1 Distribution: noble-proposed Machine Architecture: riscv64 Host Architecture: riscv64 Build Architecture: riscv64 Build Type: any I: NOTICE: Log filtering will replace 'home/buildd/build-PACKAGEBUILD-26962135/chroot-autobuild' with '<>' I: NOTICE: Log filtering will replace 'build/mathcomp-real-closed-LGyXQd/resolver-E5hsMb' with '<>' +------------------------------------------------------------------------------+ | Fetch source files | +------------------------------------------------------------------------------+ Local sources ------------- mathcomp-real-closed_1.1.4-2build1.dsc exists in .; copying to chroot I: NOTICE: Log filtering will replace 'build/mathcomp-real-closed-LGyXQd/mathcomp-real-closed-1.1.4' with '<>' I: NOTICE: Log filtering will replace 'build/mathcomp-real-closed-LGyXQd' with '<>' +------------------------------------------------------------------------------+ | Install package build dependencies | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-mathcomp-algebra, libcoq-mathcomp-bigenough, libcoq-mathcomp-field, libcoq-mathcomp-ssreflect, ocaml-dune, build-essential, fakeroot Filtered Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-mathcomp-algebra, libcoq-mathcomp-bigenough, libcoq-mathcomp-field, libcoq-mathcomp-ssreflect, ocaml-dune, build-essential, fakeroot dpkg-deb: building package 'sbuild-build-depends-main-dummy' in '/<>/apt_archive/sbuild-build-depends-main-dummy.deb'. Ign:1 copy:/<>/apt_archive ./ InRelease Get:2 copy:/<>/apt_archive ./ Release [957 B] Ign:3 copy:/<>/apt_archive ./ Release.gpg Get:4 copy:/<>/apt_archive ./ Sources [426 B] Get:5 copy:/<>/apt_archive ./ Packages [509 B] Fetched 1892 B in 1s (3008 B/s) Reading package lists... Reading package lists... Install main build dependencies (apt-based resolver) ---------------------------------------------------- Installing build dependencies Reading package lists... Building dependency tree... Reading state information... The following packages were automatically installed and are no longer required: apt-utils bash-completion ca-certificates debconf-i18n krb5-locales libgpg-error-l10n libgpm2 liblocale-gettext-perl libnss-nis libnss-nisplus libtext-charwidth-perl libtext-iconv-perl libtext-wrapi18n-perl libunistring2 openssl psmisc uuid-runtime Use 'apt autoremove' to remove them. The following additional packages will be installed: autoconf automake autopoint autotools-dev coq debhelper debugedit dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-mathcomp-algebra libcoq-mathcomp-bigenough libcoq-mathcomp-field libcoq-mathcomp-fingroup libcoq-mathcomp-solvable libcoq-mathcomp-ssreflect libcoq-stdlib libdebhelper-perl libdw1 libelf1 libexpat1 libfile-stripnondeterminism-perl libfindlib-ocaml libicu72 libmagic-mgc libmagic1 libncurses-dev libncurses6 libpipeline1 libpython3-stdlib libpython3.11-minimal libpython3.11-stdlib libstdlib-ocaml libstdlib-ocaml-dev libsub-override-perl libtool libuchardet0 libxml2 libzarith-ocaml m4 man-db media-types ocaml ocaml-base ocaml-dune ocaml-findlib ocaml-interp ocaml-nox po-debconf python3 python3-minimal python3.11 python3.11-minimal Suggested packages: autoconf-archive gnu-standards autoconf-doc coqide | proofgeneral ledit | readline-editor libcoq-core-ocaml-dev why coq-doc dh-make git gettext-doc libasprintf-dev libgettextpo-dev groff ncurses-doc libtool-doc gfortran | fortran95-compiler gcj-jdk m4-doc apparmor less www-browser ocaml-doc elpa-tuareg camlp4 libmail-box-perl python3-doc python3-tk python3-venv python3.11-venv python3.11-doc binfmt-support Recommended packages: curl | wget | lynx libarchive-cpio-perl ocaml-man libltdl-dev libfindlib-ocaml-dev ledit | readline-editor libmail-sendmail-perl The following NEW packages will be installed: autoconf automake autopoint autotools-dev coq debhelper debugedit dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libcoq-core-ocaml libcoq-mathcomp-algebra libcoq-mathcomp-bigenough libcoq-mathcomp-field libcoq-mathcomp-fingroup libcoq-mathcomp-solvable libcoq-mathcomp-ssreflect libcoq-stdlib libdebhelper-perl libdw1 libelf1 libexpat1 libfile-stripnondeterminism-perl libfindlib-ocaml libicu72 libmagic-mgc libmagic1 libncurses-dev libncurses6 libpipeline1 libpython3-stdlib libpython3.11-minimal libpython3.11-stdlib libstdlib-ocaml libstdlib-ocaml-dev libsub-override-perl libtool libuchardet0 libxml2 libzarith-ocaml m4 man-db media-types ocaml ocaml-base ocaml-dune ocaml-findlib ocaml-interp ocaml-nox po-debconf python3 python3-minimal python3.11 python3.11-minimal sbuild-build-depends-main-dummy 0 upgraded, 64 newly installed, 0 to remove and 0 not upgraded. Need to get 349 MB of archives. After this operation, 1289 MB of additional disk space will be used. Get:1 copy:/<>/apt_archive ./ sbuild-build-depends-main-dummy 0.invalid.0 [728 B] Get:2 http://ftpmaster.internal/ubuntu noble/main riscv64 libpython3.11-minimal riscv64 3.11.6-3 [834 kB] Get:3 http://ftpmaster.internal/ubuntu noble/main riscv64 libexpat1 riscv64 2.5.0-2 [78.2 kB] Get:4 http://ftpmaster.internal/ubuntu noble/main riscv64 python3.11-minimal riscv64 3.11.6-3 [2147 kB] Get:5 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 python3-minimal riscv64 3.11.4-5ubuntu1 [26.9 kB] Get:6 http://ftpmaster.internal/ubuntu noble/main riscv64 media-types all 10.1.0 [27.5 kB] Get:7 http://ftpmaster.internal/ubuntu noble/main riscv64 libpython3.11-stdlib riscv64 3.11.6-3 [1906 kB] Get:8 http://ftpmaster.internal/ubuntu noble/main riscv64 python3.11 riscv64 3.11.6-3 [579 kB] Get:9 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libpython3-stdlib riscv64 3.11.4-5ubuntu1 [9568 B] Get:10 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 python3 riscv64 3.11.4-5ubuntu1 [22.9 kB] Get:11 http://ftpmaster.internal/ubuntu noble/main riscv64 libelf1 riscv64 0.189-4 [51.9 kB] Get:12 http://ftpmaster.internal/ubuntu noble/main riscv64 libicu72 riscv64 72.1-3ubuntu3 [10.8 MB] Get:13 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 libxml2 riscv64 2.9.14+dfsg-1.3build1 [708 kB] Get:14 http://ftpmaster.internal/ubuntu noble/main riscv64 libmagic-mgc riscv64 1:5.45-2 [307 kB] Get:15 http://ftpmaster.internal/ubuntu noble/main riscv64 libmagic1 riscv64 1:5.45-2 [93.6 kB] Get:16 http://ftpmaster.internal/ubuntu noble/main riscv64 file riscv64 1:5.45-2 [21.7 kB] Get:17 http://ftpmaster.internal/ubuntu noble/main riscv64 gettext-base riscv64 0.21-13build1 [41.6 kB] Get:18 http://ftpmaster.internal/ubuntu noble/main riscv64 libuchardet0 riscv64 0.0.7-1build2 [78.9 kB] Get:19 http://ftpmaster.internal/ubuntu noble/main riscv64 groff-base riscv64 1.23.0-3 [1017 kB] Get:20 http://ftpmaster.internal/ubuntu noble/main riscv64 libncurses6 riscv64 6.4+20231016-1 [113 kB] Get:21 http://ftpmaster.internal/ubuntu noble/main riscv64 libpipeline1 riscv64 1.5.7-1 [26.8 kB] Get:22 http://ftpmaster.internal/ubuntu noble-proposed/main riscv64 man-db riscv64 2.12.0-1 [1214 kB] Get:23 http://ftpmaster.internal/ubuntu noble/main riscv64 m4 riscv64 1.4.19-4 [261 kB] Get:24 http://ftpmaster.internal/ubuntu noble/main riscv64 autoconf all 2.71-3 [339 kB] Get:25 http://ftpmaster.internal/ubuntu noble/main riscv64 autotools-dev all 20220109.1 [44.9 kB] Get:26 http://ftpmaster.internal/ubuntu noble/main riscv64 automake all 1:1.16.5-1.3 [558 kB] Get:27 http://ftpmaster.internal/ubuntu noble/main riscv64 autopoint all 0.21-13build1 [422 kB] Get:28 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-stdlib riscv64 8.17.0+dfsg-1build3 [28.4 MB] Get:29 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libstdlib-ocaml riscv64 4.14.1-1ubuntu1 [381 kB] Get:30 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-base riscv64 4.14.1-1ubuntu1 [260 kB] Get:31 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libfindlib-ocaml riscv64 1.9.6-1build3 [200 kB] Get:32 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libzarith-ocaml riscv64 1.13-2build3 [121 kB] Get:33 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-core-ocaml riscv64 8.17.0+dfsg-1build3 [27.4 MB] Get:34 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libstdlib-ocaml-dev riscv64 4.14.1-1ubuntu1 [10.4 MB] Get:35 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcompiler-libs-ocaml-dev riscv64 4.14.1-1ubuntu1 [41.5 MB] Get:36 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-interp riscv64 4.14.1-1ubuntu1 [7825 kB] Get:37 http://ftpmaster.internal/ubuntu noble/main riscv64 libncurses-dev riscv64 6.4+20231016-1 [986 kB] Get:38 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml riscv64 4.14.1-1ubuntu1 [82.2 MB] Get:39 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-nox all 4.14.1-1ubuntu1 [4716 B] Get:40 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-findlib riscv64 1.9.6-1build3 [578 kB] Get:41 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 coq riscv64 8.17.0+dfsg-1build3 [96.1 MB] Get:42 http://ftpmaster.internal/ubuntu noble/main riscv64 libdebhelper-perl all 13.11.7ubuntu1 [85.8 kB] Get:43 http://ftpmaster.internal/ubuntu noble/main riscv64 libtool all 2.4.7-7 [166 kB] Get:44 http://ftpmaster.internal/ubuntu noble/main riscv64 dh-autoreconf all 20 [16.1 kB] Get:45 http://ftpmaster.internal/ubuntu noble/main riscv64 libarchive-zip-perl all 1.68-1 [90.2 kB] Get:46 http://ftpmaster.internal/ubuntu noble/main riscv64 libsub-override-perl all 0.09-4 [8706 B] Get:47 http://ftpmaster.internal/ubuntu noble/main riscv64 libfile-stripnondeterminism-perl all 1.13.1-1 [18.1 kB] Get:48 http://ftpmaster.internal/ubuntu noble/main riscv64 dh-strip-nondeterminism all 1.13.1-1 [5362 B] Get:49 http://ftpmaster.internal/ubuntu noble/main riscv64 libdw1 riscv64 0.189-4 [234 kB] Get:50 http://ftpmaster.internal/ubuntu noble/main riscv64 debugedit riscv64 1:5.0-5 [48.8 kB] Get:51 http://ftpmaster.internal/ubuntu noble/main riscv64 dwz riscv64 0.15-1 [115 kB] Get:52 http://ftpmaster.internal/ubuntu noble/main riscv64 gettext riscv64 0.21-13build1 [867 kB] Get:53 http://ftpmaster.internal/ubuntu noble/main riscv64 intltool-debian all 0.35.0+20060710.6 [23.2 kB] Get:54 http://ftpmaster.internal/ubuntu noble/main riscv64 po-debconf all 1.0.21+nmu1 [233 kB] Get:55 http://ftpmaster.internal/ubuntu noble/main riscv64 debhelper all 13.11.7ubuntu1 [940 kB] Get:56 http://ftpmaster.internal/ubuntu noble/universe riscv64 dh-coq all 0.6 [7630 B] Get:57 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-mathcomp-ssreflect riscv64 1.17.0-1build2 [4916 kB] Get:58 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-mathcomp-fingroup riscv64 1.17.0-1build2 [2139 kB] Get:59 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-mathcomp-algebra riscv64 1.17.0-1build2 [7558 kB] Get:60 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-mathcomp-bigenough riscv64 1.0.1-10build1 [26.3 kB] Get:61 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-mathcomp-solvable riscv64 1.17.0-1build2 [5112 kB] Get:62 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 libcoq-mathcomp-field riscv64 1.17.0-1build2 [3098 kB] Get:63 http://ftpmaster.internal/ubuntu noble-proposed/universe riscv64 ocaml-dune riscv64 3.11.1-1build1 [4971 kB] Get:64 http://ftpmaster.internal/ubuntu noble/universe riscv64 dh-ocaml all 2.0 [75.7 kB] Preconfiguring packages ... Fetched 349 MB in 51s (6775 kB/s) Selecting previously unselected package libpython3.11-minimal:riscv64. (Reading database ... 13558 files and directories currently installed.) Preparing to unpack .../libpython3.11-minimal_3.11.6-3_riscv64.deb ... Unpacking libpython3.11-minimal:riscv64 (3.11.6-3) ... Selecting previously unselected package libexpat1:riscv64. Preparing to unpack .../libexpat1_2.5.0-2_riscv64.deb ... Unpacking libexpat1:riscv64 (2.5.0-2) ... Selecting previously unselected package python3.11-minimal. Preparing to unpack .../python3.11-minimal_3.11.6-3_riscv64.deb ... Unpacking python3.11-minimal (3.11.6-3) ... Setting up libpython3.11-minimal:riscv64 (3.11.6-3) ... Setting up libexpat1:riscv64 (2.5.0-2) ... Setting up python3.11-minimal (3.11.6-3) ... Selecting previously unselected package python3-minimal. (Reading database ... 13872 files and directories currently installed.) Preparing to unpack .../python3-minimal_3.11.4-5ubuntu1_riscv64.deb ... Unpacking python3-minimal (3.11.4-5ubuntu1) ... Selecting previously unselected package media-types. Preparing to unpack .../media-types_10.1.0_all.deb ... Unpacking media-types (10.1.0) ... Selecting previously unselected package libpython3.11-stdlib:riscv64. Preparing to unpack .../libpython3.11-stdlib_3.11.6-3_riscv64.deb ... Unpacking libpython3.11-stdlib:riscv64 (3.11.6-3) ... Selecting previously unselected package python3.11. Preparing to unpack .../python3.11_3.11.6-3_riscv64.deb ... Unpacking python3.11 (3.11.6-3) ... Selecting previously unselected package libpython3-stdlib:riscv64. Preparing to unpack .../libpython3-stdlib_3.11.4-5ubuntu1_riscv64.deb ... Unpacking libpython3-stdlib:riscv64 (3.11.4-5ubuntu1) ... Setting up python3-minimal (3.11.4-5ubuntu1) ... Selecting previously unselected package python3. (Reading database ... 14288 files and directories currently installed.) Preparing to unpack .../00-python3_3.11.4-5ubuntu1_riscv64.deb ... Unpacking python3 (3.11.4-5ubuntu1) ... Selecting previously unselected package libelf1:riscv64. Preparing to unpack .../01-libelf1_0.189-4_riscv64.deb ... Unpacking libelf1:riscv64 (0.189-4) ... Selecting previously unselected package libicu72:riscv64. Preparing to unpack .../02-libicu72_72.1-3ubuntu3_riscv64.deb ... Unpacking libicu72:riscv64 (72.1-3ubuntu3) ... Selecting previously unselected package libxml2:riscv64. Preparing to unpack .../03-libxml2_2.9.14+dfsg-1.3build1_riscv64.deb ... Unpacking libxml2:riscv64 (2.9.14+dfsg-1.3build1) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../04-libmagic-mgc_1%3a5.45-2_riscv64.deb ... Unpacking libmagic-mgc (1:5.45-2) ... Selecting previously unselected package libmagic1:riscv64. Preparing to unpack .../05-libmagic1_1%3a5.45-2_riscv64.deb ... Unpacking libmagic1:riscv64 (1:5.45-2) ... Selecting previously unselected package file. Preparing to unpack .../06-file_1%3a5.45-2_riscv64.deb ... Unpacking file (1:5.45-2) ... Selecting previously unselected package gettext-base. Preparing to unpack .../07-gettext-base_0.21-13build1_riscv64.deb ... Unpacking gettext-base (0.21-13build1) ... Selecting previously unselected package libuchardet0:riscv64. Preparing to unpack .../08-libuchardet0_0.0.7-1build2_riscv64.deb ... Unpacking libuchardet0:riscv64 (0.0.7-1build2) ... Selecting previously unselected package groff-base. Preparing to unpack .../09-groff-base_1.23.0-3_riscv64.deb ... Unpacking groff-base (1.23.0-3) ... Selecting previously unselected package libncurses6:riscv64. Preparing to unpack .../10-libncurses6_6.4+20231016-1_riscv64.deb ... Unpacking libncurses6:riscv64 (6.4+20231016-1) ... Selecting previously unselected package libpipeline1:riscv64. Preparing to unpack .../11-libpipeline1_1.5.7-1_riscv64.deb ... Unpacking libpipeline1:riscv64 (1.5.7-1) ... Selecting previously unselected package man-db. Preparing to unpack .../12-man-db_2.12.0-1_riscv64.deb ... Unpacking man-db (2.12.0-1) ... Selecting previously unselected package m4. Preparing to unpack .../13-m4_1.4.19-4_riscv64.deb ... Unpacking m4 (1.4.19-4) ... Selecting previously unselected package autoconf. Preparing to unpack .../14-autoconf_2.71-3_all.deb ... Unpacking autoconf (2.71-3) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../15-autotools-dev_20220109.1_all.deb ... Unpacking autotools-dev (20220109.1) ... Selecting previously unselected package automake. Preparing to unpack .../16-automake_1%3a1.16.5-1.3_all.deb ... Unpacking automake (1:1.16.5-1.3) ... Selecting previously unselected package autopoint. Preparing to unpack .../17-autopoint_0.21-13build1_all.deb ... Unpacking autopoint (0.21-13build1) ... Selecting previously unselected package libcoq-stdlib. Preparing to unpack .../18-libcoq-stdlib_8.17.0+dfsg-1build3_riscv64.deb ... Unpacking libcoq-stdlib (8.17.0+dfsg-1build3) ... Selecting previously unselected package libstdlib-ocaml. Preparing to unpack .../19-libstdlib-ocaml_4.14.1-1ubuntu1_riscv64.deb ... Unpacking libstdlib-ocaml (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-base. Preparing to unpack .../20-ocaml-base_4.14.1-1ubuntu1_riscv64.deb ... Unpacking ocaml-base (4.14.1-1ubuntu1) ... Selecting previously unselected package libfindlib-ocaml. Preparing to unpack .../21-libfindlib-ocaml_1.9.6-1build3_riscv64.deb ... Unpacking libfindlib-ocaml (1.9.6-1build3) ... Selecting previously unselected package libzarith-ocaml. Preparing to unpack .../22-libzarith-ocaml_1.13-2build3_riscv64.deb ... Unpacking libzarith-ocaml (1.13-2build3) ... Selecting previously unselected package libcoq-core-ocaml. Preparing to unpack .../23-libcoq-core-ocaml_8.17.0+dfsg-1build3_riscv64.deb ... Unpacking libcoq-core-ocaml (8.17.0+dfsg-1build3) ... Selecting previously unselected package libstdlib-ocaml-dev. Preparing to unpack .../24-libstdlib-ocaml-dev_4.14.1-1ubuntu1_riscv64.deb ... Unpacking libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... Selecting previously unselected package libcompiler-libs-ocaml-dev. Preparing to unpack .../25-libcompiler-libs-ocaml-dev_4.14.1-1ubuntu1_riscv64.deb ... Unpacking libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-interp. Preparing to unpack .../26-ocaml-interp_4.14.1-1ubuntu1_riscv64.deb ... Unpacking ocaml-interp (4.14.1-1ubuntu1) ... Selecting previously unselected package libncurses-dev:riscv64. Preparing to unpack .../27-libncurses-dev_6.4+20231016-1_riscv64.deb ... Unpacking libncurses-dev:riscv64 (6.4+20231016-1) ... Selecting previously unselected package ocaml. Preparing to unpack .../28-ocaml_4.14.1-1ubuntu1_riscv64.deb ... Unpacking ocaml (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-nox. Preparing to unpack .../29-ocaml-nox_4.14.1-1ubuntu1_all.deb ... Unpacking ocaml-nox (4.14.1-1ubuntu1) ... Selecting previously unselected package ocaml-findlib. Preparing to unpack .../30-ocaml-findlib_1.9.6-1build3_riscv64.deb ... Unpacking ocaml-findlib (1.9.6-1build3) ... Selecting previously unselected package coq. Preparing to unpack .../31-coq_8.17.0+dfsg-1build3_riscv64.deb ... Unpacking coq (8.17.0+dfsg-1build3) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../32-libdebhelper-perl_13.11.7ubuntu1_all.deb ... Unpacking libdebhelper-perl (13.11.7ubuntu1) ... Selecting previously unselected package libtool. Preparing to unpack .../33-libtool_2.4.7-7_all.deb ... Unpacking libtool (2.4.7-7) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../34-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../35-libarchive-zip-perl_1.68-1_all.deb ... Unpacking libarchive-zip-perl (1.68-1) ... Selecting previously unselected package libsub-override-perl. Preparing to unpack .../36-libsub-override-perl_0.09-4_all.deb ... Unpacking libsub-override-perl (0.09-4) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../37-libfile-stripnondeterminism-perl_1.13.1-1_all.deb ... Unpacking libfile-stripnondeterminism-perl (1.13.1-1) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../38-dh-strip-nondeterminism_1.13.1-1_all.deb ... Unpacking dh-strip-nondeterminism (1.13.1-1) ... Selecting previously unselected package libdw1:riscv64. Preparing to unpack .../39-libdw1_0.189-4_riscv64.deb ... Unpacking libdw1:riscv64 (0.189-4) ... Selecting previously unselected package debugedit. Preparing to unpack .../40-debugedit_1%3a5.0-5_riscv64.deb ... Unpacking debugedit (1:5.0-5) ... Selecting previously unselected package dwz. Preparing to unpack .../41-dwz_0.15-1_riscv64.deb ... Unpacking dwz (0.15-1) ... Selecting previously unselected package gettext. Preparing to unpack .../42-gettext_0.21-13build1_riscv64.deb ... Unpacking gettext (0.21-13build1) ... Selecting previously unselected package intltool-debian. Preparing to unpack .../43-intltool-debian_0.35.0+20060710.6_all.deb ... Unpacking intltool-debian (0.35.0+20060710.6) ... Selecting previously unselected package po-debconf. Preparing to unpack .../44-po-debconf_1.0.21+nmu1_all.deb ... Unpacking po-debconf (1.0.21+nmu1) ... Selecting previously unselected package debhelper. Preparing to unpack .../45-debhelper_13.11.7ubuntu1_all.deb ... Unpacking debhelper (13.11.7ubuntu1) ... Selecting previously unselected package dh-coq. Preparing to unpack .../46-dh-coq_0.6_all.deb ... Unpacking dh-coq (0.6) ... Selecting previously unselected package libcoq-mathcomp-ssreflect. Preparing to unpack .../47-libcoq-mathcomp-ssreflect_1.17.0-1build2_riscv64.deb ... Unpacking libcoq-mathcomp-ssreflect (1.17.0-1build2) ... Selecting previously unselected package libcoq-mathcomp-fingroup. Preparing to unpack .../48-libcoq-mathcomp-fingroup_1.17.0-1build2_riscv64.deb ... Unpacking libcoq-mathcomp-fingroup (1.17.0-1build2) ... Selecting previously unselected package libcoq-mathcomp-algebra. Preparing to unpack .../49-libcoq-mathcomp-algebra_1.17.0-1build2_riscv64.deb ... Unpacking libcoq-mathcomp-algebra (1.17.0-1build2) ... Selecting previously unselected package libcoq-mathcomp-bigenough. Preparing to unpack .../50-libcoq-mathcomp-bigenough_1.0.1-10build1_riscv64.deb ... Unpacking libcoq-mathcomp-bigenough (1.0.1-10build1) ... Selecting previously unselected package libcoq-mathcomp-solvable. Preparing to unpack .../51-libcoq-mathcomp-solvable_1.17.0-1build2_riscv64.deb ... Unpacking libcoq-mathcomp-solvable (1.17.0-1build2) ... Selecting previously unselected package libcoq-mathcomp-field. Preparing to unpack .../52-libcoq-mathcomp-field_1.17.0-1build2_riscv64.deb ... Unpacking libcoq-mathcomp-field (1.17.0-1build2) ... Selecting previously unselected package ocaml-dune. Preparing to unpack .../53-ocaml-dune_3.11.1-1build1_riscv64.deb ... Unpacking ocaml-dune (3.11.1-1build1) ... Selecting previously unselected package dh-ocaml. Preparing to unpack .../54-dh-ocaml_2.0_all.deb ... Unpacking dh-ocaml (2.0) ... Selecting previously unselected package sbuild-build-depends-main-dummy. Preparing to unpack .../55-sbuild-build-depends-main-dummy_0.invalid.0_riscv64.deb ... Unpacking sbuild-build-depends-main-dummy (0.invalid.0) ... Setting up media-types (10.1.0) ... Setting up libpipeline1:riscv64 (1.5.7-1) ... Setting up libicu72:riscv64 (72.1-3ubuntu3) ... Setting up libmagic-mgc (1:5.45-2) ... Setting up dh-coq (0.6) ... Setting up libarchive-zip-perl (1.68-1) ... Setting up libpython3.11-stdlib:riscv64 (3.11.6-3) ... Setting up libdebhelper-perl (13.11.7ubuntu1) ... Setting up dh-ocaml (2.0) ... Setting up libmagic1:riscv64 (1:5.45-2) ... Setting up gettext-base (0.21-13build1) ... Setting up m4 (1.4.19-4) ... Setting up file (1:5.45-2) ... Setting up ocaml-dune (3.11.1-1build1) ... Setting up autotools-dev (20220109.1) ... Setting up libcoq-stdlib (8.17.0+dfsg-1build3) ... Setting up libncurses6:riscv64 (6.4+20231016-1) ... Setting up libstdlib-ocaml (4.14.1-1ubuntu1) ... Setting up autopoint (0.21-13build1) ... Setting up ocaml-base (4.14.1-1ubuntu1) ... Setting up autoconf (2.71-3) ... Setting up libuchardet0:riscv64 (0.0.7-1build2) ... Setting up libsub-override-perl (0.09-4) ... Setting up libelf1:riscv64 (0.189-4) ... Setting up libxml2:riscv64 (2.9.14+dfsg-1.3build1) ... Setting up libpython3-stdlib:riscv64 (3.11.4-5ubuntu1) ... Setting up automake (1:1.16.5-1.3) ... update-alternatives: using /usr/bin/automake-1.16 to provide /usr/bin/automake (automake) in auto mode Setting up libfile-stripnondeterminism-perl (1.13.1-1) ... Setting up python3.11 (3.11.6-3) ... Setting up libdw1:riscv64 (0.189-4) ... Setting up libncurses-dev:riscv64 (6.4+20231016-1) ... Setting up gettext (0.21-13build1) ... Setting up libtool (2.4.7-7) ... Setting up libstdlib-ocaml-dev (4.14.1-1ubuntu1) ... Setting up libfindlib-ocaml (1.9.6-1build3) ... Setting up python3 (3.11.4-5ubuntu1) ... Setting up libzarith-ocaml (1.13-2build3) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up dh-autoreconf (20) ... Setting up libcompiler-libs-ocaml-dev (4.14.1-1ubuntu1) ... Setting up ocaml-interp (4.14.1-1ubuntu1) ... Setting up ocaml-findlib (1.9.6-1build3) ... Setting up dh-strip-nondeterminism (1.13.1-1) ... Setting up dwz (0.15-1) ... Setting up libcoq-core-ocaml (8.17.0+dfsg-1build3) ... Setting up groff-base (1.23.0-3) ... Setting up debugedit (1:5.0-5) ... Setting up libcoq-mathcomp-ssreflect (1.17.0-1build2) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up libcoq-mathcomp-bigenough (1.0.1-10build1) ... Setting up ocaml (4.14.1-1ubuntu1) ... Setting up man-db (2.12.0-1) ... Not building database; man-db/auto-update is not 'true'. Created symlink /etc/systemd/system/timers.target.wants/man-db.timer → /lib/systemd/system/man-db.timer. Setting up libcoq-mathcomp-fingroup (1.17.0-1build2) ... Setting up ocaml-nox (4.14.1-1ubuntu1) ... Setting up coq (8.17.0+dfsg-1build3) ... Setting up libcoq-mathcomp-algebra (1.17.0-1build2) ... Setting up debhelper (13.11.7ubuntu1) ... Setting up libcoq-mathcomp-solvable (1.17.0-1build2) ... Setting up libcoq-mathcomp-field (1.17.0-1build2) ... Setting up sbuild-build-depends-main-dummy (0.invalid.0) ... Processing triggers for systemd (253.5-1ubuntu7) ... Processing triggers for libc-bin (2.38-3ubuntu1) ... +------------------------------------------------------------------------------+ | Check architectures | +------------------------------------------------------------------------------+ Arch check ok (riscv64 included in any) +------------------------------------------------------------------------------+ | Build environment | +------------------------------------------------------------------------------+ Kernel: Linux 5.13.0-1019-generic #21~20.04.1-Ubuntu SMP Thu Mar 24 22:36:01 UTC 2022 riscv64 (riscv64) Toolchain package versions: binutils_2.41-6ubuntu1 dpkg-dev_1.22.1ubuntu2 g++-13_13.2.0-6ubuntu1 gcc-13_13.2.0-6ubuntu1 libc6-dev_2.38-3ubuntu1 libstdc++-13-dev_13.2.0-6ubuntu1 libstdc++6_13.2.0-6ubuntu1 linux-libc-dev_6.5.0-9.9 Package versions: adduser_3.137ubuntu1 advancecomp_2.5-1 apt_2.7.6 apt-utils_2.7.6 autoconf_2.71-3 automake_1:1.16.5-1.3 autopoint_0.21-13build1 autotools-dev_20220109.1 base-files_13ubuntu4 base-passwd_3.6.2 bash_5.2.15-2ubuntu2 bash-completion_1:2.11-8 binutils_2.41-6ubuntu1 binutils-common_2.41-6ubuntu1 binutils-riscv64-linux-gnu_2.41-6ubuntu1 bsdextrautils_2.39.1-4ubuntu2 bsdutils_1:2.39.1-4ubuntu2 build-essential_12.10ubuntu1 bzip2_1.0.8-5build1 ca-certificates_20230311ubuntu1 coq_8.17.0+dfsg-1build3 coreutils_9.1-1ubuntu2 cpp_4:13.2.0-1ubuntu1 cpp-13_13.2.0-6ubuntu1 dash_0.5.12-6ubuntu1 debconf_1.5.82 debconf-i18n_1.5.82 debhelper_13.11.7ubuntu1 debianutils_5.14 debugedit_1:5.0-5 dh-autoreconf_20 dh-coq_0.6 dh-ocaml_2.0 dh-strip-nondeterminism_1.13.1-1 diffutils_1:3.10-1 dpkg_1.22.1ubuntu2 dpkg-dev_1.22.1ubuntu2 dwz_0.15-1 e2fsprogs_1.47.0-2ubuntu1 fakeroot_1.32.2-1 file_1:5.45-2 findutils_4.9.0-5 g++_4:13.2.0-1ubuntu1 g++-13_13.2.0-6ubuntu1 gcc_4:13.2.0-1ubuntu1 gcc-13_13.2.0-6ubuntu1 gcc-13-base_13.2.0-6ubuntu1 gettext_0.21-13build1 gettext-base_0.21-13build1 gpg_2.2.40-1.1ubuntu1 gpg-agent_2.2.40-1.1ubuntu1 gpgconf_2.2.40-1.1ubuntu1 gpgv_2.2.40-1.1ubuntu1 grep_3.11-3 groff-base_1.23.0-3 gzip_1.12-1ubuntu1 hostname_3.23+nmu1ubuntu1 init_1.65.2ubuntu1 init-system-helpers_1.65.2ubuntu1 intltool-debian_0.35.0+20060710.6 krb5-locales_1.20.1-3ubuntu1 libacl1_2.3.1-3 libapparmor1_4.0.0~alpha2-0ubuntu6 libapt-pkg6.0_2.7.6 libarchive-zip-perl_1.68-1 libargon2-1_0~20190702+dfsg-4 libasan8_13.2.0-6ubuntu1 libassuan0_2.5.6-1 libatomic1_13.2.0-6ubuntu1 libattr1_1:2.5.1-4 libaudit-common_1:3.1.1-1build1 libaudit1_1:3.1.1-1build1 libbinutils_2.41-6ubuntu1 libblkid1_2.39.1-4ubuntu2 libbz2-1.0_1.0.8-5build1 libc-bin_2.38-3ubuntu1 libc-dev-bin_2.38-3ubuntu1 libc6_2.38-3ubuntu1 libc6-dev_2.38-3ubuntu1 libcap-ng0_0.8.3-1build3 libcap2_1:2.66-4ubuntu1 libcc1-0_13.2.0-6ubuntu1 libcom-err2_1.47.0-2ubuntu1 libcompiler-libs-ocaml-dev_4.14.1-1ubuntu1 libcoq-core-ocaml_8.17.0+dfsg-1build3 libcoq-mathcomp-algebra_1.17.0-1build2 libcoq-mathcomp-bigenough_1.0.1-10build1 libcoq-mathcomp-field_1.17.0-1build2 libcoq-mathcomp-fingroup_1.17.0-1build2 libcoq-mathcomp-solvable_1.17.0-1build2 libcoq-mathcomp-ssreflect_1.17.0-1build2 libcoq-stdlib_8.17.0+dfsg-1build3 libcrypt-dev_1:4.4.36-2 libcrypt1_1:4.4.36-2 libcryptsetup12_2:2.6.1-4ubuntu3 libctf-nobfd0_2.41-6ubuntu1 libctf0_2.41-6ubuntu1 libdb5.3_5.3.28+dfsg2-4 libdebconfclient0_0.270ubuntu1 libdebhelper-perl_13.11.7ubuntu1 libdevmapper1.02.1_2:1.02.185-2ubuntu1 libdpkg-perl_1.22.1ubuntu2 libdw1_0.189-4 libelf1_0.189-4 libexpat1_2.5.0-2 libext2fs2_1.47.0-2ubuntu1 libfakeroot_1.32.2-1 libfdisk1_2.39.1-4ubuntu2 libffi8_3.4.4-1 libfile-stripnondeterminism-perl_1.13.1-1 libfindlib-ocaml_1.9.6-1build3 libgcc-13-dev_13.2.0-6ubuntu1 libgcc-s1_13.2.0-6ubuntu1 libgcrypt20_1.10.2-3ubuntu1 libgdbm-compat4_1.23-3 libgdbm6_1.23-3 libgmp10_2:6.3.0+dfsg-2ubuntu4 libgnutls30_3.8.1-4ubuntu3 libgomp1_13.2.0-6ubuntu1 libgpg-error-l10n_1.47-2 libgpg-error0_1.47-2 libgpm2_1.20.7-10build1 libgssapi-krb5-2_1.20.1-3ubuntu1 libhogweed6_3.9.1-2 libicu72_72.1-3ubuntu3 libidn2-0_2.3.4-1build1 libip4tc2_1.8.9-2ubuntu2 libisl23_0.26-3 libjansson4_2.14-2 libjson-c5_0.17-1 libk5crypto3_1.20.1-3ubuntu1 libkeyutils1_1.6.3-2 libkmod2_30+20230519-1ubuntu3 libkrb5-3_1.20.1-3ubuntu1 libkrb5support0_1.20.1-3ubuntu1 liblocale-gettext-perl_1.07-6 liblockfile-bin_1.17-1build2 liblockfile1_1.17-1build2 liblz4-1_1.9.4-1 liblzma5_5.4.4-0.1 libmagic-mgc_1:5.45-2 libmagic1_1:5.45-2 libmd0_1.1.0-1 libmount1_2.39.1-4ubuntu2 libmpc3_1.3.1-1 libmpfr6_4.2.1-1 libncurses-dev_6.4+20231016-1 libncurses6_6.4+20231016-1 libncursesw6_6.4+20231016-1 libnettle8_3.9.1-2 libnpth0_1.6-3build2 libnsl-dev_1.3.0-3 libnsl2_1.3.0-3 libnss-nis_3.1-0ubuntu6 libnss-nisplus_1.3-0ubuntu6 libp11-kit0_0.25.0-4ubuntu1 libpam-modules_1.5.2-6ubuntu1 libpam-modules-bin_1.5.2-6ubuntu1 libpam-runtime_1.5.2-6ubuntu1 libpam0g_1.5.2-6ubuntu1 libpcre2-8-0_10.42-4 libperl5.36_5.36.0-9ubuntu1 libpipeline1_1.5.7-1 libpng16-16_1.6.40-2 libproc2-0_2:4.0.3-1ubuntu1 libpython3-stdlib_3.11.4-5ubuntu1 libpython3.11-minimal_3.11.6-3 libpython3.11-stdlib_3.11.6-3 libreadline8_8.2-1.3 libseccomp2_2.5.4-2ubuntu1 libselinux1_3.5-1build1 libsemanage-common_3.5-1build1 libsemanage2_3.5-1build1 libsepol2_3.5-1 libsframe1_2.41-6ubuntu1 libsmartcols1_2.39.1-4ubuntu2 libsqlite3-0_3.44.0-1 libss2_1.47.0-2ubuntu1 libssl3_3.0.10-1ubuntu2.1 libstdc++-13-dev_13.2.0-6ubuntu1 libstdc++6_13.2.0-6ubuntu1 libstdlib-ocaml_4.14.1-1ubuntu1 libstdlib-ocaml-dev_4.14.1-1ubuntu1 libsub-override-perl_0.09-4 libsystemd-shared_253.5-1ubuntu7 libsystemd0_253.5-1ubuntu7 libtasn1-6_4.19.0-3 libtext-charwidth-perl_0.04-11 libtext-iconv-perl_1.7-8 libtext-wrapi18n-perl_0.06-10 libtinfo6_6.4+20231016-1 libtirpc-common_1.3.4+ds-1 libtirpc-dev_1.3.4+ds-1 libtirpc3_1.3.4+ds-1 libtool_2.4.7-7 libuchardet0_0.0.7-1build2 libudev1_253.5-1ubuntu7 libunistring2_1.0-2 libunistring5_1.1-2 libuuid1_2.39.1-4ubuntu2 libxml2_2.9.14+dfsg-1.3build1 libxxhash0_0.8.2-2 libzarith-ocaml_1.13-2build3 libzstd1_1.5.5+dfsg2-2 linux-libc-dev_6.5.0-9.9 lockfile-progs_0.1.19build1 login_1:4.13+dfsg1-1ubuntu1 logsave_1.47.0-2ubuntu1 lto-disabled-list_43 m4_1.4.19-4 make_4.3-4.1build1 man-db_2.12.0-1 mawk_1.3.4.20231102-1 media-types_10.1.0 mount_2.39.1-4ubuntu2 ncurses-base_6.4+20231016-1 ncurses-bin_6.4+20231016-1 ocaml_4.14.1-1ubuntu1 ocaml-base_4.14.1-1ubuntu1 ocaml-dune_3.11.1-1build1 ocaml-findlib_1.9.6-1build3 ocaml-interp_4.14.1-1ubuntu1 ocaml-nox_4.14.1-1ubuntu1 openssl_3.0.10-1ubuntu2.1 optipng_0.7.7-3 passwd_1:4.13+dfsg1-1ubuntu1 patch_2.7.6-7build2 perl_5.36.0-9ubuntu1 perl-base_5.36.0-9ubuntu1 perl-modules-5.36_5.36.0-9ubuntu1 pinentry-curses_1.2.1-1ubuntu1 pkgbinarymangler_154 po-debconf_1.0.21+nmu1 policyrcd-script-zg2_0.1-3.1 procps_2:4.0.3-1ubuntu1 psmisc_23.6-1 python3_3.11.4-5ubuntu1 python3-minimal_3.11.4-5ubuntu1 python3.11_3.11.6-3 python3.11-minimal_3.11.6-3 readline-common_8.2-1.3 rpcsvc-proto_1.4.2-0ubuntu6 sbuild-build-depends-main-dummy_0.invalid.0 sed_4.9-1 sensible-utils_0.0.20 systemd_253.5-1ubuntu7 systemd-dev_253.5-1ubuntu7 systemd-sysv_253.5-1ubuntu7 sysvinit-utils_3.07-1ubuntu1 tar_1.34+dfsg-1.2ubuntu1 tzdata_2023c-9ubuntu1 ubuntu-keyring_2021.03.26 usrmerge_35ubuntu1 util-linux_2.39.1-4ubuntu2 uuid-runtime_2.39.1-4ubuntu2 xz-utils_5.4.4-0.1 zlib1g_1:1.2.13.dfsg-1ubuntu5 +------------------------------------------------------------------------------+ | Build | +------------------------------------------------------------------------------+ Unpack source ------------- -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 Format: 3.0 (quilt) Source: mathcomp-real-closed Binary: libcoq-mathcomp-real-closed Architecture: any Version: 1.1.4-2build1 Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Homepage: https://github.com/math-comp/real-closed Standards-Version: 4.6.2 Vcs-Browser: https://salsa.debian.org/ocaml-team/mathcomp-real-closed Vcs-Git: https://salsa.debian.org/ocaml-team/mathcomp-real-closed.git Testsuite: autopkgtest Testsuite-Triggers: coq Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-mathcomp-algebra, libcoq-mathcomp-bigenough, libcoq-mathcomp-field, libcoq-mathcomp-ssreflect, ocaml-dune Package-List: libcoq-mathcomp-real-closed deb ocaml optional arch=any Checksums-Sha1: abe6b9b77b870b5fb889fa45990d6f69090988cf 120543 mathcomp-real-closed_1.1.4.orig.tar.gz bf08ea8d6ff404ea3772a8e904fc8421a9213c14 8864 mathcomp-real-closed_1.1.4-2build1.debian.tar.xz Checksums-Sha256: cf36400e474fd4b894c190b98bb9d332fe99e17f71e2b8e875f98a16d759154c 120543 mathcomp-real-closed_1.1.4.orig.tar.gz 95dc1f5606bd42d2d50ae971ab93d049cc54d9444ecbaed852def90c45e0c65c 8864 mathcomp-real-closed_1.1.4-2build1.debian.tar.xz Files: 7f4de4355b0ae3b23886f2222fdf9e12 120543 mathcomp-real-closed_1.1.4.orig.tar.gz 742c981b5932ff6c60358667a7eb8462 8864 mathcomp-real-closed_1.1.4-2build1.debian.tar.xz -----BEGIN PGP SIGNATURE----- iQIzBAEBCAAdFiEEkpeKbhleSSGCX3/w808JdE6fXdkFAmVGmDoACgkQ808JdE6f XdnRvBAAot/rI3+3OtOou8ujFCcqF4vA2CD7oBXHNP7BQ3eLDXgZcojpkIdH27Ya 6Sn8B8wArWeLzZU8taeoFhHx6Pp6PUXycTjCsGkiTwyqcBDzpdKdp6hgpvbmZ5qX JGRuoG4iNbbcUDxSj7n40nlDs6mdZokp8/JFJrVmnjbjc97aKUmCOs8PC6p5Jj2V aBq4C8DLDLlBwqADMdffqLtXsqJksb2EnG5EgYxYLhc4ANEB6aD51JDtyahc03h/ wY2DL+6uuMAjguEybIjokyYQr8C69BPMTAmApw59GutZd/vezHtmE8yXte7nukaq E9PBBDRjGqg6vZoiZpsWRfeeXO2i/9pAZfnWY4gwgoyyU3BnCRTm559QJFxHYlUK ZtvHPSR1e8eYjj9XHbYE0lSOtv9k2fYsUZl6ofYmUYbtcd7toO8z18xqumfJ4hq0 5l6TboatvxactD6T3ra/JftHsIoBS6inHIK3o/2rS6haEcZSqMsAOZK32ySDmLud yhztAKxOaPs7gcwY4/YSw4Q03Ct8PMjHwav9CKsQA7/pXa2FIXct4GRZHQMOVF1G R7pTO87HgmDicm9vFvHlA7XG41wshQkDRh0ueuq+6EHC0G74cEVC9FcTgHFzvHX7 MncpXEcG+cy+e9PcFmUOREN+GTQMh7eh+jyJju2uhbMFhK8NnuM= =uby+ -----END PGP SIGNATURE----- gpgv: Signature made Sat Nov 4 19:15:06 2023 UTC gpgv: using RSA key 92978A6E195E4921825F7FF0F34F09744E9F5DD9 gpgv: Can't check signature: No public key dpkg-source: warning: cannot verify inline signature for ./mathcomp-real-closed_1.1.4-2build1.dsc: no acceptable signature found dpkg-source: info: extracting mathcomp-real-closed in /<> dpkg-source: info: unpacking mathcomp-real-closed_1.1.4.orig.tar.gz dpkg-source: info: unpacking mathcomp-real-closed_1.1.4-2build1.debian.tar.xz Check disk space ---------------- Sufficient free space for build User Environment ---------------- APT_CONFIG=/var/lib/sbuild/apt.conf DEB_BUILD_OPTIONS=parallel=8 HOME=/sbuild-nonexistent LANG=C.UTF-8 LC_ALL=C.UTF-8 LOGNAME=buildd PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games SCHROOT_ALIAS_NAME=build-PACKAGEBUILD-26962135 SCHROOT_CHROOT_NAME=build-PACKAGEBUILD-26962135 SCHROOT_COMMAND=env SCHROOT_GID=2501 SCHROOT_GROUP=buildd SCHROOT_SESSION_ID=build-PACKAGEBUILD-26962135 SCHROOT_UID=2001 SCHROOT_USER=buildd SHELL=/bin/sh TERM=unknown USER=buildd V=1 dpkg-buildpackage ----------------- Command: dpkg-buildpackage -us -uc -mLaunchpad Build Daemon -B -rfakeroot dpkg-buildpackage: info: source package mathcomp-real-closed dpkg-buildpackage: info: source version 1.1.4-2build1 dpkg-buildpackage: info: source distribution noble dpkg-source --before-build . dpkg-buildpackage: info: host architecture riscv64 debian/rules clean dh clean --with coq debian/rules override_dh_auto_clean make[1]: Entering directory '/<>' make clean make[2]: Entering directory '/<>' coq_makefile -f _CoqProject -o Makefile.coq make --no-print-directory -f Makefile.coq clean CLEAN make[2]: Leaving directory '/<>' rm -f Makefile.coq Makefile.coq.conf make[1]: Leaving directory '/<>' dh_clean debian/rules binary-arch dh binary-arch --with coq dh_update_autotools_config -a dh_autoreconf -a dh_auto_configure -a debian/rules override_dh_auto_build make[1]: Entering directory '/<>' make make[2]: Entering directory '/<>' coq_makefile -f _CoqProject -o Makefile.coq make --no-print-directory -f Makefile.coq COQDEP VFILES COQC theories/polyorder.v COQC theories/cauchyreals.v File "./theories/cauchyreals.v", line 76, characters 8-17: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 76, characters 8-17: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 76, characters 8-17: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 84, characters 13-22: Warning: Notation ler_pmulr is deprecated since mathcomp 1.17.0. Use ler_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 84, characters 37-45: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 84, characters 13-22: Warning: Notation ler_pmulr is deprecated since mathcomp 1.17.0. Use ler_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 84, characters 13-22: Warning: Notation ler_pmulr is deprecated since mathcomp 1.17.0. Use ler_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 86, characters 19-31: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 86, characters 47-54: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 86, characters 19-31: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 86, characters 19-31: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 86, characters 47-54: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 86, characters 47-54: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 89, characters 14-25: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 92, characters 8-19: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 92, characters 8-19: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 92, characters 8-19: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 95, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 95, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 95, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 95, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 95, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 97, characters 11-19: Warning: Notation ler_oppl is deprecated since mathcomp 1.17.0. Use lerNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 97, characters 11-19: Warning: Notation ler_oppl is deprecated since mathcomp 1.17.0. Use lerNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 97, characters 11-19: Warning: Notation ler_oppl is deprecated since mathcomp 1.17.0. Use lerNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 102, characters 8-17: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 102, characters 8-17: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 102, characters 8-17: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 121, characters 27-36: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 121, characters 27-36: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 121, characters 27-36: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 132, characters 35-46: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 132, characters 35-46: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 132, characters 35-46: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 133, characters 6-17: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 135, characters 37-48: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 135, characters 37-48: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 135, characters 37-48: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 139, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 139, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 139, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 140, characters 39-46: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 140, characters 39-46: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 140, characters 39-46: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 142, characters 17-27: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 142, characters 17-27: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 142, characters 17-27: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 144, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 144, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 144, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 145, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 145, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 145, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 146, characters 11-22: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 146, characters 11-22: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 146, characters 11-22: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 152, characters 10-19: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 152, characters 10-19: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 152, characters 10-19: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 214, characters 10-19: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 214, characters 10-19: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 214, characters 10-19: Warning: Notation ltr_paddr is deprecated since mathcomp 1.17.0. Use ltr_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 233, characters 27-36: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 233, characters 27-36: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 233, characters 27-36: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 246, characters 8-22: Warning: Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 246, characters 8-22: Warning: Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 246, characters 8-22: Warning: Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 250, characters 45-56: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 251, characters 6-17: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 253, characters 37-48: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 253, characters 37-48: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 253, characters 37-48: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 257, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 257, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 257, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 258, characters 39-46: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 258, characters 39-46: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 258, characters 39-46: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 260, characters 10-20: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 260, characters 10-20: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 260, characters 10-20: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 262, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 262, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 262, characters 21-33: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 263, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 263, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 263, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 264, characters 11-22: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 264, characters 11-22: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 264, characters 11-22: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 317, characters 37-45: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 317, characters 37-45: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 317, characters 37-45: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 325, characters 37-45: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 325, characters 37-45: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 325, characters 37-45: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 39-47: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 48-62: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 339, characters 9-23: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 39-47: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 39-47: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 48-62: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 48-62: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 39-47: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 39-47: Warning: Notation ltr_oppr is deprecated since mathcomp 1.17.0. Use ltrNr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 48-62: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 338, characters 48-62: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 339, characters 9-23: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 339, characters 9-23: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 339, characters 9-23: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 339, characters 9-23: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 358, characters 8-22: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 358, characters 8-22: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 358, characters 8-22: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 361, characters 29-39: Warning: Notation ler_muln2r is deprecated since mathcomp 1.17.0. Use lerMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 361, characters 29-39: Warning: Notation ler_muln2r is deprecated since mathcomp 1.17.0. Use lerMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 361, characters 29-39: Warning: Notation ler_muln2r is deprecated since mathcomp 1.17.0. Use lerMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 361, characters 29-39: Warning: Notation ler_muln2r is deprecated since mathcomp 1.17.0. Use lerMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 361, characters 29-39: Warning: Notation ler_muln2r is deprecated since mathcomp 1.17.0. Use lerMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 367, characters 29-38: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 367, characters 29-38: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 367, characters 29-38: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 368, characters 30-39: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 368, characters 30-39: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 368, characters 30-39: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 371, characters 27-36: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 371, characters 27-36: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 371, characters 27-36: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 372, characters 28-37: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 372, characters 28-37: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 372, characters 28-37: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 395, characters 15-25: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 395, characters 15-25: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 395, characters 15-25: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 400, characters 21-32: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 400, characters 21-32: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 400, characters 21-32: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 401, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 401, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 401, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 406, characters 19-30: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 406, characters 19-30: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 406, characters 19-30: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 425, characters 8-22: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 425, characters 8-22: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 425, characters 8-22: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 430, characters 30-39: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 430, characters 30-39: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 430, characters 30-39: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 432, characters 30-39: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 432, characters 30-39: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 432, characters 30-39: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 434, characters 49-58: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 434, characters 49-58: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 434, characters 49-58: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 439, characters 10-17: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 439, characters 10-17: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 439, characters 10-17: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 440, characters 34-43: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 440, characters 34-43: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 440, characters 34-43: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 443, characters 14-28: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 443, characters 14-28: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 443, characters 14-28: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 447, characters 33-42: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 447, characters 33-42: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 447, characters 33-42: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 447, characters 33-42: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 447, characters 33-42: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 449, characters 45-52: Warning: Notation ltr_add is deprecated since mathcomp 1.17.0. Use ltrD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 449, characters 45-52: Warning: Notation ltr_add is deprecated since mathcomp 1.17.0. Use ltrD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 449, characters 45-52: Warning: Notation ltr_add is deprecated since mathcomp 1.17.0. Use ltrD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 450, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 450, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 450, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 452, characters 9-23: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 452, characters 9-23: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 452, characters 9-23: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 540, characters 46-53: Warning: Notation ltr_add is deprecated since mathcomp 1.17.0. Use ltrD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 540, characters 46-53: Warning: Notation ltr_add is deprecated since mathcomp 1.17.0. Use ltrD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 540, characters 46-53: Warning: Notation ltr_add is deprecated since mathcomp 1.17.0. Use ltrD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 547, characters 46-58: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 547, characters 46-58: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 547, characters 46-58: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 551, characters 46-58: Warning: Notation ler_norm_sub is deprecated since mathcomp 1.17.0. Use ler_normB instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 551, characters 46-58: Warning: Notation ler_norm_sub is deprecated since mathcomp 1.17.0. Use ler_normB instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 551, characters 46-58: Warning: Notation ler_norm_sub is deprecated since mathcomp 1.17.0. Use ler_normB instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 556, characters 35-47: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 556, characters 35-47: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 556, characters 35-47: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 22-34: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 48-58: Warning: Notation ltr_le_add is deprecated since mathcomp 1.17.0. Use ltr_leD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 22-34: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 22-34: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 48-58: Warning: Notation ltr_le_add is deprecated since mathcomp 1.17.0. Use ltr_leD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 48-58: Warning: Notation ltr_le_add is deprecated since mathcomp 1.17.0. Use ltr_leD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 48-58: Warning: Notation ltr_le_add is deprecated since mathcomp 1.17.0. Use ltr_leD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 588, characters 48-58: Warning: Notation ltr_le_add is deprecated since mathcomp 1.17.0. Use ltr_leD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 589, characters 32-42: Warning: Notation ler_lt_add is deprecated since mathcomp 1.17.0. Use ler_ltD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 589, characters 32-42: Warning: Notation ler_lt_add is deprecated since mathcomp 1.17.0. Use ler_ltD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 589, characters 32-42: Warning: Notation ler_lt_add is deprecated since mathcomp 1.17.0. Use ler_ltD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 744, characters 13-22: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 744, characters 13-22: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 744, characters 13-22: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 753, characters 13-22: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 753, characters 13-22: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 753, characters 13-22: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 769, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 769, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 769, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 769, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 769, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 788, characters 54-63: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 788, characters 54-63: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 788, characters 54-63: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 790, characters 16-24: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 790, characters 16-24: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 790, characters 16-24: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 800, characters 46-56: Warning: Notation ltr_spaddr is deprecated since mathcomp 1.17.0. Use ltr_pwDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 820, characters 58-66: Warning: Notation ltr_addl is deprecated since mathcomp 1.17.0. Use ltrDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 851, characters 32-41: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 851, characters 32-41: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 851, characters 32-41: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 877, characters 28-38: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 877, characters 28-38: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 877, characters 28-38: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 885, characters 11-24: Warning: Notation ler_subl_addr is deprecated since mathcomp 1.17.0. Use lerBlDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 885, characters 11-24: Warning: Notation ler_subl_addr is deprecated since mathcomp 1.17.0. Use lerBlDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 885, characters 11-24: Warning: Notation ler_subl_addr is deprecated since mathcomp 1.17.0. Use lerBlDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 907, characters 10-21: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 908, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 908, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 908, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 910, characters 23-34: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 911, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 911, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 911, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 927, characters 13-23: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 927, characters 13-23: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 927, characters 13-23: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 931, characters 10-21: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 931, characters 10-21: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 931, characters 10-21: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 933, characters 27-38: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 935, characters 13-24: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 935, characters 13-24: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 935, characters 13-24: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 956, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 956, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 956, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 970, characters 14-24: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 975, characters 12-26: Warning: Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 975, characters 12-26: Warning: Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 975, characters 12-26: Warning: Notation ler_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 983, characters 14-28: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 983, characters 14-28: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 983, characters 14-28: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 984, characters 17-28: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 984, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 984, characters 17-28: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 984, characters 17-28: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 984, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 984, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 985, characters 35-46: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 985, characters 35-46: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 985, characters 35-46: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 986, characters 15-24: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 986, characters 15-24: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 986, characters 15-24: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1030, characters 10-21: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1031, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1031, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1031, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1033, characters 23-34: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1034, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1034, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1034, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1045, characters 13-23: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1045, characters 13-23: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1045, characters 13-23: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1048, characters 12-23: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1048, characters 12-23: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1048, characters 12-23: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1050, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1050, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1050, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1051, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1051, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1051, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1077, characters 19-28: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1077, characters 19-28: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1077, characters 19-28: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1079, characters 41-50: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1079, characters 41-50: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1079, characters 41-50: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1081, characters 35-44: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1081, characters 35-44: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1081, characters 35-44: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1083, characters 17-27: Warning: Notation ler_lt_add is deprecated since mathcomp 1.17.0. Use ler_ltD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1083, characters 44-53: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1083, characters 17-27: Warning: Notation ler_lt_add is deprecated since mathcomp 1.17.0. Use ler_ltD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1083, characters 17-27: Warning: Notation ler_lt_add is deprecated since mathcomp 1.17.0. Use ler_ltD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1083, characters 44-53: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1083, characters 44-53: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1084, characters 47-55: Warning: Notation ltr_addr is deprecated since mathcomp 1.17.0. Use ltrDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1084, characters 47-55: Warning: Notation ltr_addr is deprecated since mathcomp 1.17.0. Use ltrDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1084, characters 47-55: Warning: Notation ltr_addr is deprecated since mathcomp 1.17.0. Use ltrDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1084, characters 47-55: Warning: Notation ltr_addr is deprecated since mathcomp 1.17.0. Use ltrDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1109, characters 14-23: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1109, characters 14-23: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1109, characters 14-23: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1112, characters 12-21: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1112, characters 12-21: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1112, characters 12-21: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1122, characters 46-55: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1122, characters 46-55: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1122, characters 46-55: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1136, characters 19-28: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1136, characters 19-28: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1136, characters 19-28: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1223, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1223, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1223, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1224, characters 13-24: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1224, characters 13-24: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1224, characters 13-24: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1233, characters 16-30: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1233, characters 16-30: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1233, characters 16-30: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1235, characters 20-31: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1235, characters 20-31: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1235, characters 20-31: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1252, characters 32-41: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1252, characters 32-41: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1252, characters 32-41: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1253, characters 25-37: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1253, characters 25-37: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1253, characters 25-37: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1254, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1254, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1254, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1273, characters 13-24: Warning: Notation ltr_pexpn2r is deprecated since mathcomp 1.17.0. Use ltr_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1273, characters 13-24: Warning: Notation ltr_pexpn2r is deprecated since mathcomp 1.17.0. Use ltr_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1273, characters 13-24: Warning: Notation ltr_pexpn2r is deprecated since mathcomp 1.17.0. Use ltr_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1330, characters 19-33: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1330, characters 19-33: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1330, characters 19-33: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1332, characters 30-41: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1332, characters 30-41: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1332, characters 30-41: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1333, characters 12-21: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1333, characters 44-56: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1333, characters 12-21: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1333, characters 12-21: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1333, characters 44-56: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1333, characters 44-56: Warning: Notation ler_norm_add is deprecated since mathcomp 1.17.0. Use ler_normD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1334, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1334, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1334, characters 30-39: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1372, characters 19-28: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1372, characters 19-28: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1372, characters 19-28: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1374, characters 34-43: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1374, characters 34-43: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1374, characters 34-43: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1375, characters 28-40: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1375, characters 28-40: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1375, characters 28-40: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1376, characters 17-24: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1376, characters 17-24: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1376, characters 17-24: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1382, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1382, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1382, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1383, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1383, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1383, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1384, characters 21-31: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1384, characters 21-31: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1384, characters 21-31: Warning: Notation ltr_pmul2r is deprecated since mathcomp 1.17.0. Use ltr_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1385, characters 15-24: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1385, characters 15-24: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1385, characters 15-24: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1393, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1393, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1393, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1394, characters 26-38: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1394, characters 26-38: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1394, characters 26-38: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1395, characters 15-22: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1395, characters 15-22: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1395, characters 15-22: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1397, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1397, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1397, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1398, characters 26-38: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1398, characters 26-38: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1398, characters 26-38: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1399, characters 15-22: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1399, characters 15-22: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1399, characters 15-22: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1400, characters 10-19: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1400, characters 10-19: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1400, characters 10-19: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1403, characters 54-63: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1403, characters 54-63: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1403, characters 54-63: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1404, characters 52-61: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1404, characters 52-61: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1404, characters 52-61: Warning: Notation ltr_add2r is deprecated since mathcomp 1.17.0. Use ltrD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1406, characters 43-52: Warning: Notation ltr_add2l is deprecated since mathcomp 1.17.0. Use ltrD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1406, characters 53-63: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1406, characters 43-52: Warning: Notation ltr_add2l is deprecated since mathcomp 1.17.0. Use ltrD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1406, characters 43-52: Warning: Notation ltr_add2l is deprecated since mathcomp 1.17.0. Use ltrD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1406, characters 53-63: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1406, characters 53-63: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1408, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1408, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1408, characters 20-27: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1409, characters 13-27: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1409, characters 13-27: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1409, characters 13-27: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1410, characters 23-35: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1410, characters 23-35: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1410, characters 23-35: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1412, characters 30-37: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1412, characters 30-37: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1412, characters 30-37: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1413, characters 16-30: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1413, characters 16-30: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1413, characters 16-30: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1414, characters 13-27: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1414, characters 13-27: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1414, characters 13-27: Warning: Notation ler_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ler_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1477, characters 8-15: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1477, characters 8-15: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1477, characters 8-15: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1483, characters 8-19: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1483, characters 8-19: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1483, characters 8-19: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1495, characters 33-44: Warning: Notation ler_pmuln2r is deprecated since mathcomp 1.17.0. Use ler_pMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1495, characters 33-44: Warning: Notation ler_pmuln2r is deprecated since mathcomp 1.17.0. Use ler_pMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1495, characters 33-44: Warning: Notation ler_pmuln2r is deprecated since mathcomp 1.17.0. Use ler_pMn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1496, characters 51-62: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1496, characters 51-62: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1496, characters 51-62: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1498, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1498, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1498, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1516, characters 10-21: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1516, characters 10-21: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1516, characters 10-21: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1519, characters 25-36: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1519, characters 25-36: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1519, characters 25-36: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1522, characters 8-19: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1522, characters 50-57: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1522, characters 8-19: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1522, characters 8-19: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1522, characters 50-57: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1522, characters 50-57: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1548, characters 17-28: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1548, characters 17-28: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1548, characters 17-28: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1549, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1549, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1549, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1556, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1556, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1556, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1557, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1557, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1557, characters 11-25: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1583, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1583, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1583, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1584, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1584, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1584, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1587, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1587, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1587, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1588, characters 11-25: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1588, characters 11-25: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1588, characters 11-25: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1607, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1607, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1607, characters 17-28: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1608, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1608, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1608, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1611, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1611, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1611, characters 15-26: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1612, characters 11-25: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1612, characters 11-25: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/cauchyreals.v", line 1612, characters 11-25: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] COQC theories/polyrcf.v File "./theories/polyrcf.v", line 132, characters 29-39: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 132, characters 29-39: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 132, characters 29-39: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 10-19: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 10-19: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 10-19: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 135, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 136, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 136, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 136, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 137, characters 28-36: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 137, characters 28-36: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 137, characters 28-36: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 154, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 154, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 154, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 10-19: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 10-19: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 10-19: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 157, characters 56-66: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 158, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 158, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 158, characters 13-23: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 159, characters 52-61: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 159, characters 52-61: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 159, characters 52-61: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 161, characters 11-20: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 161, characters 11-20: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 161, characters 11-20: Warning: Notation ler_paddl is deprecated since mathcomp 1.17.0. Use ler_wpDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 175, characters 24-34: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 175, characters 24-34: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 175, characters 24-34: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 179, characters 28-42: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 179, characters 28-42: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 179, characters 28-42: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 180, characters 42-50: Warning: Notation ler_addr is deprecated since mathcomp 1.17.0. Use lerDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 180, characters 42-50: Warning: Notation ler_addr is deprecated since mathcomp 1.17.0. Use lerDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 180, characters 42-50: Warning: Notation ler_addr is deprecated since mathcomp 1.17.0. Use lerDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 182, characters 8-22: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 182, characters 58-67: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 182, characters 8-22: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 182, characters 8-22: Warning: Notation ler_pdivl_mull is deprecated since mathcomp 1.17.0. Use ler_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 182, characters 58-67: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 182, characters 58-67: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 185, characters 5-15: Warning: Notation ler_pmul2r is deprecated since mathcomp 1.17.0. Use ler_pM2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 191, characters 25-33: Warning: Notation ler_pmul is deprecated since mathcomp 1.17.0. Use ler_pM instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 191, characters 48-59: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 191, characters 25-33: Warning: Notation ler_pmul is deprecated since mathcomp 1.17.0. Use ler_pM instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 191, characters 25-33: Warning: Notation ler_pmul is deprecated since mathcomp 1.17.0. Use ler_pM instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 191, characters 48-59: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 191, characters 48-59: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 198, characters 57-65: Warning: Notation ltr_oppl is deprecated since mathcomp 1.17.0. Use ltrNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 198, characters 57-65: Warning: Notation ltr_oppl is deprecated since mathcomp 1.17.0. Use ltrNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 198, characters 57-65: Warning: Notation ltr_oppl is deprecated since mathcomp 1.17.0. Use ltrNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 205, characters 57-65: Warning: Notation ltr_oppl is deprecated since mathcomp 1.17.0. Use ltrNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 205, characters 57-65: Warning: Notation ltr_oppl is deprecated since mathcomp 1.17.0. Use ltrNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 205, characters 57-65: Warning: Notation ltr_oppl is deprecated since mathcomp 1.17.0. Use ltrNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 210, characters 18-28: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 210, characters 18-28: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 210, characters 18-28: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 292, characters 13-22: Warning: Notation ler_eexpr is deprecated since mathcomp 1.17.0. Use ler_eXnr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 292, characters 13-22: Warning: Notation ler_eexpr is deprecated since mathcomp 1.17.0. Use ler_eXnr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 292, characters 13-22: Warning: Notation ler_eexpr is deprecated since mathcomp 1.17.0. Use ler_eXnr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 307, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 307, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 307, characters 13-27: Warning: Notation ltr_pdivl_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivlMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 313, characters 13-24: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 313, characters 43-53: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 313, characters 13-24: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 313, characters 13-24: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 313, characters 43-53: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 313, characters 43-53: Warning: Notation ler_expn2r is deprecated since mathcomp 1.17.0. Use lerXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 314, characters 21-30: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 314, characters 21-30: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 314, characters 21-30: Warning: Notation gtr_pmulr is deprecated since mathcomp 1.17.0. Use gtr_pMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 315, characters 8-22: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 315, characters 8-22: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 315, characters 8-22: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 317, characters 22-35: Warning: Notation ltr_subl_addr is deprecated since mathcomp 1.17.0. Use ltrBlDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 317, characters 22-35: Warning: Notation ltr_subl_addr is deprecated since mathcomp 1.17.0. Use ltrBlDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 317, characters 22-35: Warning: Notation ltr_subl_addr is deprecated since mathcomp 1.17.0. Use ltrBlDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 318, characters 40-52: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 318, characters 40-52: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 318, characters 40-52: Warning: Notation ler_sub_dist is deprecated since mathcomp 1.17.0. Use lerB_dist instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 427, characters 8-16: Warning: Notation ler_addr is deprecated since mathcomp 1.17.0. Use lerDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 427, characters 8-16: Warning: Notation ler_addr is deprecated since mathcomp 1.17.0. Use lerDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 427, characters 8-16: Warning: Notation ler_addr is deprecated since mathcomp 1.17.0. Use lerDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 444, characters 8-16: Warning: Notation ltr_addr is deprecated since mathcomp 1.17.0. Use ltrDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 444, characters 8-16: Warning: Notation ltr_addr is deprecated since mathcomp 1.17.0. Use ltrDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 444, characters 8-16: Warning: Notation ltr_addr is deprecated since mathcomp 1.17.0. Use ltrDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 540, characters 35-43: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 540, characters 35-43: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 540, characters 35-43: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 711, characters 23-31: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 711, characters 23-31: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 711, characters 23-31: Warning: Notation ltr_opp2 is deprecated since mathcomp 1.17.0. Use ltrN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1526, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1526, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1526, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1540, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1540, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1540, characters 13-23: Warning: Notation ltr_spaddl is deprecated since mathcomp 1.17.0. Use ltr_pwDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1698, characters 49-57: Warning: Notation ler_oppl is deprecated since mathcomp 1.17.0. Use lerNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1698, characters 49-57: Warning: Notation ler_oppl is deprecated since mathcomp 1.17.0. Use lerNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1698, characters 49-57: Warning: Notation ler_oppl is deprecated since mathcomp 1.17.0. Use lerNl instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1699, characters 21-29: Warning: Notation ler_opp2 is deprecated since mathcomp 1.17.0. Use lerN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1699, characters 21-29: Warning: Notation ler_opp2 is deprecated since mathcomp 1.17.0. Use lerN2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/polyrcf.v", line 1699, characters 21-29: Warning: Notation ler_opp2 is deprecated since mathcomp 1.17.0. Use lerN2 instead. [deprecated-syntactic-definition,deprecated] COQC theories/realalg.v File "./theories/realalg.v", line 48, characters 20-27: Warning: Notation rmorphX is deprecated since mathcomp 1.17.0. Use rmorphXn instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 48, characters 20-27: Warning: Notation rmorphX is deprecated since mathcomp 1.17.0. Use rmorphXn instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 48, characters 20-27: Warning: Notation rmorphX is deprecated since mathcomp 1.17.0. Use rmorphXn instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 407, characters 21-32: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 407, characters 36-50: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 407, characters 21-32: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 407, characters 21-32: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 407, characters 36-50: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 407, characters 36-50: Warning: Notation ler_pdivr_mull is deprecated since mathcomp 1.17.0. Use ler_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 409, characters 13-21: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 409, characters 13-21: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 409, characters 13-21: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 413, characters 19-31: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 413, characters 19-31: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 413, characters 19-31: Warning: Notation ler_dist_add is deprecated since mathcomp 1.17.0. Use ler_distD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 414, characters 8-15: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 414, characters 8-15: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 414, characters 8-15: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 415, characters 30-41: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 428, characters 10-24: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 428, characters 36-50: Warning: Notation ltr_pdivr_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 428, characters 10-24: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 428, characters 10-24: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 428, characters 36-50: Warning: Notation ltr_pdivr_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 428, characters 36-50: Warning: Notation ltr_pdivr_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivrMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 16-24: Warning: Notation lef_pinv is deprecated since mathcomp 1.17.0. Use lef_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 48-59: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 16-24: Warning: Notation lef_pinv is deprecated since mathcomp 1.17.0. Use lef_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 16-24: Warning: Notation lef_pinv is deprecated since mathcomp 1.17.0. Use lef_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 16-24: Warning: Notation lef_pinv is deprecated since mathcomp 1.17.0. Use lef_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 16-24: Warning: Notation lef_pinv is deprecated since mathcomp 1.17.0. Use lef_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 16-24: Warning: Notation lef_pinv is deprecated since mathcomp 1.17.0. Use lef_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 48-59: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 443, characters 48-59: Warning: Notation ler_eexpn2l is deprecated since mathcomp 1.17.0. Use ler_eXn2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 444, characters 13-23: Warning: Notation ltr_pmul2l is deprecated since mathcomp 1.17.0. Use ltr_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 444, characters 13-23: Warning: Notation ltr_pmul2l is deprecated since mathcomp 1.17.0. Use ltr_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 444, characters 13-23: Warning: Notation ltr_pmul2l is deprecated since mathcomp 1.17.0. Use ltr_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 446, characters 41-49: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 446, characters 41-49: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 446, characters 41-49: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 446, characters 41-49: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 446, characters 41-49: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 446, characters 41-49: Warning: Notation ger_addl is deprecated since mathcomp 1.17.0. Use gerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 447, characters 14-28: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 447, characters 14-28: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 447, characters 14-28: Warning: Notation ltr_pdivr_mulr is deprecated since mathcomp 1.17.0. Use ltr_pdivrMr instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 456, characters 37-45: Warning: Notation ltf_pinv is deprecated since mathcomp 1.17.0. Use ltf_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 456, characters 37-45: Warning: Notation ltf_pinv is deprecated since mathcomp 1.17.0. Use ltf_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 456, characters 37-45: Warning: Notation ltf_pinv is deprecated since mathcomp 1.17.0. Use ltf_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 477, characters 55-65: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 487, characters 10-21: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 487, characters 10-21: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 487, characters 10-21: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 546, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 546, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 546, characters 13-27: Warning: Notation ltr_pdivl_mull is deprecated since mathcomp 1.17.0. Use ltr_pdivlMl instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 867, characters 22-29: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 867, characters 22-29: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 867, characters 22-29: Warning: Notation ler_add is deprecated since mathcomp 1.17.0. Use lerD instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 879, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 879, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 879, characters 15-26: Warning: Notation ler_wpmul2l is deprecated since mathcomp 1.17.0. Use ler_wpM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 880, characters 13-24: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 880, characters 13-24: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 880, characters 13-24: Warning: Notation ler_wpmul2r is deprecated since mathcomp 1.17.0. Use ler_wpM2rinstead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 898, characters 35-44: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 898, characters 35-44: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 898, characters 35-44: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 902, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 902, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 902, characters 32-41: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1026, characters 43-52: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1026, characters 43-52: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1026, characters 43-52: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1246, characters 26-34: Warning: Notation ltf_pinv is deprecated since mathcomp 1.17.0. Use ltf_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1246, characters 26-34: Warning: Notation ltf_pinv is deprecated since mathcomp 1.17.0. Use ltf_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1246, characters 26-34: Warning: Notation ltf_pinv is deprecated since mathcomp 1.17.0. Use ltf_pV2 instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1358, characters 40-49: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1358, characters 40-49: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/realalg.v", line 1358, characters 40-49: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] COQC theories/complex.v File "./theories/complex.v", line 25, characters 0-27: Warning: The default and global localities for this command outside sections are currently equivalent to the combination of the standard meaning of "global" (as described in the reference manual), "export" and re-exporting for every surrounding module. It will change to just "global" (with the meaning used by the "Set" command) in a future release. To preserve the current meaning in a forward compatible way, use the attribute "#[global,export]" and repeat the command with just "#[export]" in any surrounding modules. If you are fine with the change of semantics, disable this warning. [deprecated-tacopt-without-locality,deprecated] File "./theories/complex.v", line 332, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 332, characters 43-52: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 334, characters 20-29: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 335, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 335, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 335, characters 42-51: Warning: Notation ler_add2r is deprecated since mathcomp 1.17.0. Use lerD2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 343, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 343, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 343, characters 11-22: Warning: Notation ler_pexpn2r is deprecated since mathcomp 1.17.0. Use ler_pXn2r instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 345, characters 40-49: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 346, characters 36-46: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 346, characters 36-46: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 346, characters 36-46: Warning: Notation ler_pmul2l is deprecated since mathcomp 1.17.0. Use ler_pM2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 347, characters 53-62: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 347, characters 53-62: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 347, characters 53-62: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 348, characters 39-48: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 348, characters 39-48: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 348, characters 39-48: Warning: Notation ler_add2l is deprecated since mathcomp 1.17.0. Use lerD2l instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 519, characters 29-36: Warning: Notation rmorphX is deprecated since mathcomp 1.17.0. Use rmorphXn instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 519, characters 29-36: Warning: Notation rmorphX is deprecated since mathcomp 1.17.0. Use rmorphXn instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 519, characters 29-36: Warning: Notation rmorphX is deprecated since mathcomp 1.17.0. Use rmorphXn instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 665, characters 13-22: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 665, characters 13-22: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 665, characters 13-22: Warning: Notation ler_paddr is deprecated since mathcomp 1.17.0. Use ler_wpDr instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 720, characters 59-67: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 720, characters 59-67: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] File "./theories/complex.v", line 720, characters 59-67: Warning: Notation ler_addl is deprecated since mathcomp 1.17.0. Use lerDl instead. [deprecated-syntactic-definition,deprecated] COQC theories/ordered_qelim.v COQC theories/mxtens.v COQC theories/qe_rcf_th.v COQC theories/qe_rcf.v COQC theories/all_real_closed.v make[2]: Leaving directory '/<>' dune build Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. make[1]: Leaving directory '/<>' dh: command-omitted: The call to "debian/rules override_dh_auto_test" was omitted due to "DEB_BUILD_OPTIONS=nocheck" create-stamp debian/debhelper-build-stamp dh_prep -a debian/rules override_dh_auto_install make[1]: Entering directory '/<>' make install DESTDIR=/<>/debian/tmp make[2]: Entering directory '/<>' coq_makefile -f _CoqProject -o Makefile.coq make --no-print-directory -f Makefile.coq install INSTALL theories/all_real_closed.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/cauchyreals.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/complex.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/ordered_qelim.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/polyorder.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/polyrcf.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/qe_rcf_th.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/qe_rcf.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/realalg.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/mxtens.vo /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/all_real_closed.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/cauchyreals.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/complex.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/ordered_qelim.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/polyorder.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/polyrcf.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/qe_rcf_th.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/qe_rcf.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/realalg.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/mxtens.v /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/all_real_closed.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/cauchyreals.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/complex.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/ordered_qelim.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/polyorder.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/polyrcf.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/qe_rcf_th.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/qe_rcf.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/realalg.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ INSTALL theories/mxtens.glob /<>/debian/tmp//usr/lib/ocaml/coq//user-contrib/mathcomp/real_closed/ make[2]: Leaving directory '/<>' dune install --destdir=/<>/debian/tmp --prefix=/usr --libdir=/usr/lib/ocaml Warning: Coq Language Versions lower than 0.8 have been deprecated in Dune 3.8 and will be removed in an upcoming Dune version. make[1]: Leaving directory '/<>' dh_install -a dh_installdocs -a dh_installchangelogs -a dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a dh_missing -a dh_dwz -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_coq -a dh_gencontrol -a dh_md5sums -a dh_builddeb -a INFO: pkgstriptranslations version 154 pkgstriptranslations: processing libcoq-mathcomp-real-closed (in debian/libcoq-mathcomp-real-closed); do_strip: , oemstrip: pkgmaintainermangler: Maintainer field overridden to "Ubuntu Developers " pkgstripfiles: processing control file: debian/libcoq-mathcomp-real-closed/DEBIAN/control, package libcoq-mathcomp-real-closed, directory debian/libcoq-mathcomp-real-closed pkgstripfiles: Running PNG optimization (using 8 cpus) for package libcoq-mathcomp-real-closed ... pkgstripfiles: No PNG files. dpkg-deb: building package 'libcoq-mathcomp-real-closed' in '../libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb'. dpkg-genbuildinfo --build=any -O../mathcomp-real-closed_1.1.4-2build1_riscv64.buildinfo dpkg-genchanges --build=any -mLaunchpad Build Daemon -O../mathcomp-real-closed_1.1.4-2build1_riscv64.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) -------------------------------------------------------------------------------- Build finished at 2023-11-16T02:37:25Z Finished -------- I: Built successfully +------------------------------------------------------------------------------+ | Changes | +------------------------------------------------------------------------------+ mathcomp-real-closed_1.1.4-2build1_riscv64.changes: --------------------------------------------------- Format: 1.8 Date: Sat, 04 Nov 2023 20:15:05 +0100 Source: mathcomp-real-closed Binary: libcoq-mathcomp-real-closed Built-For-Profiles: noudeb Architecture: riscv64 Version: 1.1.4-2build1 Distribution: noble-proposed Urgency: medium Maintainer: Launchpad Build Daemon Changed-By: Gianfranco Costamagna Description: libcoq-mathcomp-real-closed - Real closed fields for Mathematical Components Changes: mathcomp-real-closed (1.1.4-2build1) noble; urgency=medium . * Rebuild against new OCAML ABI. Checksums-Sha1: 2c0bd8cef44e6908ec87b4caed9bf58b59b4a54e 2631126 libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb 93601e790758454acc92b9f463d7c93106aa43f4 6604 mathcomp-real-closed_1.1.4-2build1_riscv64.buildinfo Checksums-Sha256: 96c6c98e8e36ff38c515f0abe39035c1315fe00855f2ad4a9d5770d915caefb6 2631126 libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb 3438094d4960a98a4087d8f1b9d660c59f18a919404234c1ce79582f2172c039 6604 mathcomp-real-closed_1.1.4-2build1_riscv64.buildinfo Files: 62028823da1bf12c43be45e923922c40 2631126 ocaml optional libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb 4224cb2240ebca47b155907416cd306c 6604 ocaml optional mathcomp-real-closed_1.1.4-2build1_riscv64.buildinfo /<>/mathcomp-real-closed_1.1.4-2build1_riscv64.changes.new could not be renamed to /<>/mathcomp-real-closed_1.1.4-2build1_riscv64.changes: Illegal seek Distribution field may be wrong!!! +------------------------------------------------------------------------------+ | Buildinfo | +------------------------------------------------------------------------------+ Format: 1.0 Source: mathcomp-real-closed Binary: libcoq-mathcomp-real-closed Architecture: riscv64 Version: 1.1.4-2build1 Checksums-Md5: 62028823da1bf12c43be45e923922c40 2631126 libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb Checksums-Sha1: 2c0bd8cef44e6908ec87b4caed9bf58b59b4a54e 2631126 libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb Checksums-Sha256: 96c6c98e8e36ff38c515f0abe39035c1315fe00855f2ad4a9d5770d915caefb6 2631126 libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb Build-Origin: Ubuntu Build-Architecture: riscv64 Build-Date: Thu, 16 Nov 2023 02:37:17 +0000 Build-Path: /<> Build-Tainted-By: merged-usr-via-aliased-dirs usr-local-has-programs Installed-Build-Depends: autoconf (= 2.71-3), automake (= 1:1.16.5-1.3), autopoint (= 0.21-13build1), autotools-dev (= 20220109.1), base-files (= 13ubuntu4), base-passwd (= 3.6.2), bash (= 5.2.15-2ubuntu2), binutils (= 2.41-6ubuntu1), binutils-common (= 2.41-6ubuntu1), binutils-riscv64-linux-gnu (= 2.41-6ubuntu1), bsdextrautils (= 2.39.1-4ubuntu2), bsdutils (= 1:2.39.1-4ubuntu2), build-essential (= 12.10ubuntu1), bzip2 (= 1.0.8-5build1), coq (= 8.17.0+dfsg-1build3), coreutils (= 9.1-1ubuntu2), cpp (= 4:13.2.0-1ubuntu1), cpp-13 (= 13.2.0-6ubuntu1), dash (= 0.5.12-6ubuntu1), debconf (= 1.5.82), debhelper (= 13.11.7ubuntu1), debianutils (= 5.14), debugedit (= 1:5.0-5), dh-autoreconf (= 20), dh-coq (= 0.6), dh-ocaml (= 2.0), dh-strip-nondeterminism (= 1.13.1-1), diffutils (= 1:3.10-1), dpkg (= 1.22.1ubuntu2), dpkg-dev (= 1.22.1ubuntu2), dwz (= 0.15-1), file (= 1:5.45-2), findutils (= 4.9.0-5), g++ (= 4:13.2.0-1ubuntu1), g++-13 (= 13.2.0-6ubuntu1), gcc (= 4:13.2.0-1ubuntu1), gcc-13 (= 13.2.0-6ubuntu1), gcc-13-base (= 13.2.0-6ubuntu1), gettext (= 0.21-13build1), gettext-base (= 0.21-13build1), grep (= 3.11-3), groff-base (= 1.23.0-3), gzip (= 1.12-1ubuntu1), hostname (= 3.23+nmu1ubuntu1), init-system-helpers (= 1.65.2ubuntu1), intltool-debian (= 0.35.0+20060710.6), libacl1 (= 2.3.1-3), libarchive-zip-perl (= 1.68-1), libasan8 (= 13.2.0-6ubuntu1), libatomic1 (= 13.2.0-6ubuntu1), libattr1 (= 1:2.5.1-4), libaudit-common (= 1:3.1.1-1build1), libaudit1 (= 1:3.1.1-1build1), libbinutils (= 2.41-6ubuntu1), libblkid1 (= 2.39.1-4ubuntu2), libbz2-1.0 (= 1.0.8-5build1), libc-bin (= 2.38-3ubuntu1), libc-dev-bin (= 2.38-3ubuntu1), libc6 (= 2.38-3ubuntu1), libc6-dev (= 2.38-3ubuntu1), libcap-ng0 (= 0.8.3-1build3), libcap2 (= 1:2.66-4ubuntu1), libcc1-0 (= 13.2.0-6ubuntu1), libcom-err2 (= 1.47.0-2ubuntu1), libcompiler-libs-ocaml-dev (= 4.14.1-1ubuntu1), libcoq-core-ocaml (= 8.17.0+dfsg-1build3), libcoq-mathcomp-algebra (= 1.17.0-1build2), libcoq-mathcomp-bigenough (= 1.0.1-10build1), libcoq-mathcomp-field (= 1.17.0-1build2), libcoq-mathcomp-fingroup (= 1.17.0-1build2), libcoq-mathcomp-solvable (= 1.17.0-1build2), libcoq-mathcomp-ssreflect (= 1.17.0-1build2), libcoq-stdlib (= 8.17.0+dfsg-1build3), libcrypt-dev (= 1:4.4.36-2), libcrypt1 (= 1:4.4.36-2), libctf-nobfd0 (= 2.41-6ubuntu1), libctf0 (= 2.41-6ubuntu1), libdb5.3 (= 5.3.28+dfsg2-4), libdebconfclient0 (= 0.270ubuntu1), libdebhelper-perl (= 13.11.7ubuntu1), libdpkg-perl (= 1.22.1ubuntu2), libdw1 (= 0.189-4), libelf1 (= 0.189-4), libexpat1 (= 2.5.0-2), libffi8 (= 3.4.4-1), libfile-stripnondeterminism-perl (= 1.13.1-1), libfindlib-ocaml (= 1.9.6-1build3), libgcc-13-dev (= 13.2.0-6ubuntu1), libgcc-s1 (= 13.2.0-6ubuntu1), libgcrypt20 (= 1.10.2-3ubuntu1), libgdbm-compat4 (= 1.23-3), libgdbm6 (= 1.23-3), libgmp10 (= 2:6.3.0+dfsg-2ubuntu4), libgomp1 (= 13.2.0-6ubuntu1), libgpg-error0 (= 1.47-2), libgssapi-krb5-2 (= 1.20.1-3ubuntu1), libicu72 (= 72.1-3ubuntu3), libisl23 (= 0.26-3), libjansson4 (= 2.14-2), libk5crypto3 (= 1.20.1-3ubuntu1), libkeyutils1 (= 1.6.3-2), libkrb5-3 (= 1.20.1-3ubuntu1), libkrb5support0 (= 1.20.1-3ubuntu1), liblz4-1 (= 1.9.4-1), liblzma5 (= 5.4.4-0.1), libmagic-mgc (= 1:5.45-2), libmagic1 (= 1:5.45-2), libmd0 (= 1.1.0-1), libmount1 (= 2.39.1-4ubuntu2), libmpc3 (= 1.3.1-1), libmpfr6 (= 4.2.1-1), libncurses-dev (= 6.4+20231016-1), libncurses6 (= 6.4+20231016-1), libncursesw6 (= 6.4+20231016-1), libnsl-dev (= 1.3.0-3), libnsl2 (= 1.3.0-3), libpam-modules (= 1.5.2-6ubuntu1), libpam-modules-bin (= 1.5.2-6ubuntu1), libpam-runtime (= 1.5.2-6ubuntu1), libpam0g (= 1.5.2-6ubuntu1), libpcre2-8-0 (= 10.42-4), libperl5.36 (= 5.36.0-9ubuntu1), libpipeline1 (= 1.5.7-1), libpython3-stdlib (= 3.11.4-5ubuntu1), libpython3.11-minimal (= 3.11.6-3), libpython3.11-stdlib (= 3.11.6-3), libreadline8 (= 8.2-1.3), libselinux1 (= 3.5-1build1), libsframe1 (= 2.41-6ubuntu1), libsmartcols1 (= 2.39.1-4ubuntu2), libsqlite3-0 (= 3.44.0-1), libssl3 (= 3.0.10-1ubuntu2.1), libstdc++-13-dev (= 13.2.0-6ubuntu1), libstdc++6 (= 13.2.0-6ubuntu1), libstdlib-ocaml (= 4.14.1-1ubuntu1), libstdlib-ocaml-dev (= 4.14.1-1ubuntu1), libsub-override-perl (= 0.09-4), libsystemd0 (= 253.5-1ubuntu7), libtinfo6 (= 6.4+20231016-1), libtirpc-common (= 1.3.4+ds-1), libtirpc-dev (= 1.3.4+ds-1), libtirpc3 (= 1.3.4+ds-1), libtool (= 2.4.7-7), libuchardet0 (= 0.0.7-1build2), libudev1 (= 253.5-1ubuntu7), libunistring5 (= 1.1-2), libuuid1 (= 2.39.1-4ubuntu2), libxml2 (= 2.9.14+dfsg-1.3build1), libzarith-ocaml (= 1.13-2build3), libzstd1 (= 1.5.5+dfsg2-2), linux-libc-dev (= 6.5.0-9.9), login (= 1:4.13+dfsg1-1ubuntu1), lto-disabled-list (= 43), m4 (= 1.4.19-4), make (= 4.3-4.1build1), man-db (= 2.12.0-1), mawk (= 1.3.4.20231102-1), media-types (= 10.1.0), ncurses-base (= 6.4+20231016-1), ncurses-bin (= 6.4+20231016-1), ocaml (= 4.14.1-1ubuntu1), ocaml-base (= 4.14.1-1ubuntu1), ocaml-dune (= 3.11.1-1build1), ocaml-findlib (= 1.9.6-1build3), ocaml-interp (= 4.14.1-1ubuntu1), ocaml-nox (= 4.14.1-1ubuntu1), patch (= 2.7.6-7build2), perl (= 5.36.0-9ubuntu1), perl-base (= 5.36.0-9ubuntu1), perl-modules-5.36 (= 5.36.0-9ubuntu1), po-debconf (= 1.0.21+nmu1), python3 (= 3.11.4-5ubuntu1), python3-minimal (= 3.11.4-5ubuntu1), python3.11 (= 3.11.6-3), python3.11-minimal (= 3.11.6-3), readline-common (= 8.2-1.3), rpcsvc-proto (= 1.4.2-0ubuntu6), sed (= 4.9-1), sensible-utils (= 0.0.20), sysvinit-utils (= 3.07-1ubuntu1), tar (= 1.34+dfsg-1.2ubuntu1), tzdata (= 2023c-9ubuntu1), util-linux (= 2.39.1-4ubuntu2), xz-utils (= 5.4.4-0.1), zlib1g (= 1:1.2.13.dfsg-1ubuntu5) Environment: DEB_BUILD_OPTIONS="nocheck parallel=8" DEB_BUILD_PROFILES="noudeb" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1699125305" +------------------------------------------------------------------------------+ | Package contents | +------------------------------------------------------------------------------+ libcoq-mathcomp-real-closed_1.1.4-2build1_riscv64.deb ----------------------------------------------------- new Debian package, version 2.0. size 2631126 bytes: control archive=1771 bytes. 1119 bytes, 23 lines control 3584 bytes, 37 lines md5sums Package: libcoq-mathcomp-real-closed Source: mathcomp-real-closed Version: 1.1.4-2build1 Architecture: riscv64 Maintainer: Ubuntu Developers Original-Maintainer: Debian OCaml Maintainers Installed-Size: 9448 Depends: libcoq-mathcomp-algebra-osx68, libcoq-mathcomp-bigenough-5a4q9, libcoq-mathcomp-field-7wil1, libcoq-mathcomp-ssreflect-blqw9 Suggests: ocaml-findlib Provides: libcoq-mathcomp-real-closed-mvy72 Section: ocaml Priority: optional Homepage: https://github.com/math-comp/real-closed Description: Real closed fields for Mathematical Components This library contains definitions and theorems about real closed fields for Mathematical Components. It includes a construction of the real and algebraic closure (with a proof of the fundamental theorem of algebra). The decidability of the first order theory of real closed field, through quantifier elimination is also established. . The Mathematical Components library is a coherent repository of general-purpose formalized mathematical theories for the Coq proof assistant. drwxr-xr-x root/root 0 2023-11-04 19:15 ./ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/lib/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/lib/ocaml/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/lib/ocaml/coq-mathcomp-real-closed/ -rw-r--r-- root/root 0 2023-11-04 19:15 ./usr/lib/ocaml/coq-mathcomp-real-closed/META -rw-r--r-- root/root 219 2023-11-04 19:15 ./usr/lib/ocaml/coq-mathcomp-real-closed/dune-package -rw-r--r-- root/root 1214 2023-11-04 19:15 ./usr/lib/ocaml/coq-mathcomp-real-closed/opam drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/lib/ocaml/coq/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/ -rw-r--r-- root/root 515 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/all_real_closed.glob -rw-r--r-- root/root 227 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/all_real_closed.v -rw-r--r-- root/root 21930 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/all_real_closed.vo -rw-r--r-- root/root 740042 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/cauchyreals.glob -rw-r--r-- root/root 65299 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/cauchyreals.v -rw-r--r-- root/root 547764 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/cauchyreals.vo -rw-r--r-- root/root 1207926 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/complex.glob -rw-r--r-- root/root 50274 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/complex.v -rw-r--r-- root/root 580627 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/complex.vo -rw-r--r-- root/root 117269 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/mxtens.glob -rw-r--r-- root/root 11604 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/mxtens.v -rw-r--r-- root/root 136243 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/mxtens.vo -rw-r--r-- root/root 278672 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/ordered_qelim.glob -rw-r--r-- root/root 48880 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/ordered_qelim.v -rw-r--r-- root/root 398856 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/ordered_qelim.vo -rw-r--r-- root/root 83794 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/polyorder.glob -rw-r--r-- root/root 9828 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/polyorder.v -rw-r--r-- root/root 81268 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/polyorder.vo -rw-r--r-- root/root 750353 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/polyrcf.glob -rw-r--r-- root/root 67864 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/polyrcf.v -rw-r--r-- root/root 996323 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/polyrcf.vo -rw-r--r-- root/root 423141 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/qe_rcf.glob -rw-r--r-- root/root 34426 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/qe_rcf.v -rw-r--r-- root/root 300283 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/qe_rcf.vo -rw-r--r-- root/root 750815 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/qe_rcf_th.glob -rw-r--r-- root/root 54430 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/qe_rcf_th.v -rw-r--r-- root/root 742073 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/qe_rcf_th.vo -rw-r--r-- root/root 511944 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/realalg.glob -rw-r--r-- root/root 59909 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/realalg.v -rw-r--r-- root/root 538548 2023-11-04 19:15 ./usr/lib/ocaml/coq/user-contrib/mathcomp/real_closed/realalg.vo drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/share/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/share/doc/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./usr/share/doc/libcoq-mathcomp-real-closed/ -rw-r--r-- root/root 2351 2023-11-04 19:15 ./usr/share/doc/libcoq-mathcomp-real-closed/README.md.gz -rw-r--r-- root/root 520 2023-11-04 19:15 ./usr/share/doc/libcoq-mathcomp-real-closed/changelog.Debian.gz -rw-r--r-- root/root 22348 2023-07-24 06:21 ./usr/share/doc/libcoq-mathcomp-real-closed/copyright drwxr-xr-x root/root 0 2023-11-04 19:15 ./var/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./var/lib/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./var/lib/coq/ drwxr-xr-x root/root 0 2023-11-04 19:15 ./var/lib/coq/md5sums/ -rw-r--r-- root/root 5 2023-11-04 19:15 ./var/lib/coq/md5sums/libcoq-mathcomp-real-closed.checksum +------------------------------------------------------------------------------+ | Post Build | +------------------------------------------------------------------------------+ +------------------------------------------------------------------------------+ | Cleanup | +------------------------------------------------------------------------------+ Purging /<> Not removing build depends: as requested +------------------------------------------------------------------------------+ | Summary | +------------------------------------------------------------------------------+ Build Architecture: riscv64 Build Type: any Build-Space: 41544 Build-Time: 1575 Distribution: noble-proposed Host Architecture: riscv64 Install-Time: 515 Job: mathcomp-real-closed_1.1.4-2build1.dsc Machine Architecture: riscv64 Package: mathcomp-real-closed Package-Time: 2118 Source-Version: 1.1.4-2build1 Space: 41544 Status: successful Version: 1.1.4-2build1 -------------------------------------------------------------------------------- Finished at 2023-11-16T02:37:25Z Build needed 00:35:18, 41544k disk space RUN: /usr/share/launchpad-buildd/bin/in-target scan-for-processes --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962135 Scanning for processes to kill in build PACKAGEBUILD-26962135 RUN: /usr/share/launchpad-buildd/bin/in-target umount-chroot --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962135 Stopping target for build PACKAGEBUILD-26962135 RUN: /usr/share/launchpad-buildd/bin/in-target remove-build --backend=chroot --series=noble --arch=riscv64 PACKAGEBUILD-26962135 Removing build PACKAGEBUILD-26962135