sbuild (Debian sbuild) 0.88.1 (16 December 2024) on derowd.up7.fr +===============================================================================+ | mathcomp-zify 1.5.0+2.0+8.16-4+ocaml1 (amd64) Wed, 15 Jan 2025 15:51:27 +0000 | +===============================================================================+ Package: mathcomp-zify Version: 1.5.0+2.0+8.16-4+ocaml1 Source Version: 1.5.0+2.0+8.16-4+ocaml1 Distribution: unstable Machine Architecture: amd64 Host Architecture: amd64 Build Architecture: amd64 Build Type: full I: No tarballs found in /home/steph/.cache/sbuild I: Unpacking /home/steph/ocaml-transitions/20250115/ocaml-5.3.0/ben/rootfs.tar.zst to /var/tmp/tmp.sbuild.qQtwMtCLX8... I: Setting up the chroot... I: Creating chroot session... I: Setting up log color... I: Setting up apt archive... +------------------------------------------------------------------------------+ | Update chroot Wed, 15 Jan 2025 15:51:34 +0000 | +------------------------------------------------------------------------------+ Ign:1 file:/rebuilt ./ InRelease Get:2 file:/rebuilt ./ Release [1351 B] Get:2 file:/rebuilt ./ Release [1351 B] Ign:3 file:/rebuilt ./ Release.gpg Get:4 file:/rebuilt ./ Packages [1294 kB] Get:5 http://localhost:9999/debian unstable InRelease [205 kB] Get:6 http://localhost:9999/debian unstable/non-free-firmware amd64 Packages [6912 B] Get:7 http://localhost:9999/debian unstable/contrib amd64 Packages [65.7 kB] Get:8 http://localhost:9999/debian unstable/main amd64 Packages [9979 kB] Get:9 http://localhost:9999/debian unstable/non-free amd64 Packages [122 kB] Fetched 10.4 MB in 1s (12.2 MB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... Calculating upgrade... 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. +------------------------------------------------------------------------------+ | Fetch source files Wed, 15 Jan 2025 15:51:36 +0000 | +------------------------------------------------------------------------------+ Local sources ------------- /tmp/tmp.ben.transition-scripts.DShdWCKr3y/mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc exists in /tmp/tmp.ben.transition-scripts.DShdWCKr3y; copying to chroot +------------------------------------------------------------------------------+ | Install package build dependencies Wed, 15 Jan 2025 15:51:37 +0000 | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-mathcomp-algebra, build-essential, fakeroot Filtered Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-mathcomp-algebra, build-essential, fakeroot dpkg-deb: warning: root directory /build/reproducible-path/resolver-vLRgxa/sbuild-build-depends-main-dummy has unusual owner or group 998:999 dpkg-deb: Hint: you might need to pass --root-owner-group, see for further details dpkg-deb: warning: ignoring 1 warning about the control file(s) dpkg-deb: building package 'sbuild-build-depends-main-dummy' in '/build/reproducible-path/resolver-vLRgxa/apt_archive/sbuild-build-depends-main-dummy.deb'. Ign:1 copy:/build/reproducible-path/resolver-vLRgxa/apt_archive ./ InRelease Get:2 copy:/build/reproducible-path/resolver-vLRgxa/apt_archive ./ Release [609 B] Ign:3 copy:/build/reproducible-path/resolver-vLRgxa/apt_archive ./ Release.gpg Get:4 copy:/build/reproducible-path/resolver-vLRgxa/apt_archive ./ Sources [665 B] Get:5 copy:/build/reproducible-path/resolver-vLRgxa/apt_archive ./ Packages [697 B] Fetched 1971 B in 0s (0 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 additional packages will be installed: autoconf automake autopoint autotools-dev bsdextrautils coq debhelper dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz fakeroot file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libconfig-tiny-perl libcoq-core-ocaml libcoq-core-ocaml-dev libcoq-elpi libcoq-hierarchy-builder libcoq-mathcomp-algebra libcoq-mathcomp-fingroup libcoq-mathcomp-ssreflect libcoq-stdlib libdebhelper-perl libelf1t64 libelpi-ocaml libelpi-ocaml-dev libexpat1 libfakeroot libffi8 libfile-stripnondeterminism-perl libfindlib-ocaml libfindlib-ocaml-dev libgmp-dev libgmp3-dev libgmpxx4ldbl libicu72 libmagic-mgc libmagic1t64 libmenhir-ocaml-dev libncurses-dev libncurses6 libncursesw6 libocaml-compiler-libs-ocaml-dev libpipeline1 libppx-derivers-ocaml-dev libppx-deriving-ocaml libppx-deriving-ocaml-dev libppxlib-ocaml-dev libpython3-stdlib libpython3.13-minimal libpython3.13-stdlib libre-ocaml-dev libreadline8t64 libsexplib0-ocaml libsexplib0-ocaml-dev libsqlite3-0 libstdlib-ocaml libstdlib-ocaml-dev libtool libuchardet0 libunistring5 libxml2 libzarith-ocaml libzarith-ocaml-dev libzstd-dev m4 man-db media-types netbase ocaml ocaml-base ocaml-findlib ocaml-interp po-debconf python3 python3-minimal python3.13 python3.13-minimal readline-common sensible-utils tzdata Suggested packages: autoconf-archive gnu-standards autoconf-doc coqide | proofgeneral ledit | readline-editor why coq-doc dh-make git gettext-doc libasprintf-dev libgettextpo-dev groff gmp-doc libgmp10-doc libmpfr-dev 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.13-venv python3.13-doc binfmt-support readline-doc Recommended packages: curl | wget | lynx libarchive-cpio-perl libgpm2 ocaml-man libltdl-dev ledit | readline-editor libmail-sendmail-perl ca-certificates The following NEW packages will be installed: autoconf automake autopoint autotools-dev bsdextrautils coq debhelper dh-autoreconf dh-coq dh-ocaml dh-strip-nondeterminism dwz fakeroot file gettext gettext-base groff-base intltool-debian libarchive-zip-perl libcompiler-libs-ocaml-dev libconfig-tiny-perl libcoq-core-ocaml libcoq-core-ocaml-dev libcoq-elpi libcoq-hierarchy-builder libcoq-mathcomp-algebra libcoq-mathcomp-fingroup libcoq-mathcomp-ssreflect libcoq-stdlib libdebhelper-perl libelf1t64 libelpi-ocaml libelpi-ocaml-dev libexpat1 libfakeroot libffi8 libfile-stripnondeterminism-perl libfindlib-ocaml libfindlib-ocaml-dev libgmp-dev libgmp3-dev libgmpxx4ldbl libicu72 libmagic-mgc libmagic1t64 libmenhir-ocaml-dev libncurses-dev libncurses6 libncursesw6 libocaml-compiler-libs-ocaml-dev libpipeline1 libppx-derivers-ocaml-dev libppx-deriving-ocaml libppx-deriving-ocaml-dev libppxlib-ocaml-dev libpython3-stdlib libpython3.13-minimal libpython3.13-stdlib libre-ocaml-dev libreadline8t64 libsexplib0-ocaml libsexplib0-ocaml-dev libsqlite3-0 libstdlib-ocaml libstdlib-ocaml-dev libtool libuchardet0 libunistring5 libxml2 libzarith-ocaml libzarith-ocaml-dev libzstd-dev m4 man-db media-types netbase ocaml ocaml-base ocaml-findlib ocaml-interp po-debconf python3 python3-minimal python3.13 python3.13-minimal readline-common sbuild-build-depends-main-dummy sensible-utils tzdata 0 upgraded, 89 newly installed, 0 to remove and 0 not upgraded. Need to get 30.1 MB/390 MB of archives. After this operation, 1258 MB of additional disk space will be used. Get:1 copy:/build/reproducible-path/resolver-vLRgxa/apt_archive ./ sbuild-build-depends-main-dummy 0.invalid.0 [904 B] Get:2 file:/rebuilt ./ libcoq-stdlib 8.20.0+dfsg-1+ocaml1 [23.5 MB] Get:3 http://localhost:9999/debian unstable/main amd64 libpython3.13-minimal amd64 3.13.1-3 [858 kB] Get:4 http://localhost:9999/debian unstable/main amd64 libexpat1 amd64 2.6.4-1 [106 kB] Get:5 http://localhost:9999/debian unstable/main amd64 python3.13-minimal amd64 3.13.1-3 [2202 kB] Get:6 http://localhost:9999/debian unstable/main amd64 python3-minimal amd64 3.13.1-2 [27.0 kB] Get:7 file:/rebuilt ./ libstdlib-ocaml 5.3.0-1~exp2+ocaml1 [604 kB] Get:8 http://localhost:9999/debian unstable/main amd64 media-types all 10.1.0 [26.9 kB] Get:9 http://localhost:9999/debian unstable/main amd64 netbase all 6.4 [12.8 kB] Get:10 http://localhost:9999/debian unstable/main amd64 tzdata all 2024b-6 [257 kB] Get:11 http://localhost:9999/debian unstable/main amd64 libffi8 amd64 3.4.6-1 [23.6 kB] Get:12 file:/rebuilt ./ ocaml-base 5.3.0-1~exp2+ocaml1 [494 kB] Get:13 http://localhost:9999/debian unstable/main amd64 libncursesw6 amd64 6.5-2+b1 [136 kB] Get:14 http://localhost:9999/debian unstable/main amd64 readline-common all 8.2-6 [69.4 kB] Get:15 http://localhost:9999/debian unstable/main amd64 libreadline8t64 amd64 8.2-6 [169 kB] Get:16 file:/rebuilt ./ libfindlib-ocaml 1.9.6-3+ocaml1 [180 kB] Get:17 http://localhost:9999/debian unstable/main amd64 libsqlite3-0 amd64 3.46.1-1 [913 kB] Get:18 file:/rebuilt ./ libzarith-ocaml 1.14-1+ocaml1 [117 kB] Get:19 file:/rebuilt ./ libcoq-core-ocaml 8.20.0+dfsg-1+ocaml1 [26.0 MB] Get:20 http://localhost:9999/debian unstable/main amd64 libpython3.13-stdlib amd64 3.13.1-3 [1973 kB] Get:21 http://localhost:9999/debian unstable/main amd64 python3.13 amd64 3.13.1-3 [740 kB] Get:22 http://localhost:9999/debian unstable/main amd64 libpython3-stdlib amd64 3.13.1-2 [9952 B] Get:23 http://localhost:9999/debian unstable/main amd64 python3 amd64 3.13.1-2 [28.0 kB] Get:24 http://localhost:9999/debian unstable/main amd64 sensible-utils all 0.0.24 [24.8 kB] Get:25 http://localhost:9999/debian unstable/main amd64 libmagic-mgc amd64 1:5.45-3+b1 [314 kB] Get:26 http://localhost:9999/debian unstable/main amd64 libmagic1t64 amd64 1:5.45-3+b1 [108 kB] Get:27 http://localhost:9999/debian unstable/main amd64 file amd64 1:5.45-3+b1 [43.3 kB] Get:28 http://localhost:9999/debian unstable/main amd64 gettext-base amd64 0.22.5-4 [200 kB] Get:29 http://localhost:9999/debian unstable/main amd64 libuchardet0 amd64 0.0.8-1+b2 [68.9 kB] Get:30 http://localhost:9999/debian unstable/main amd64 groff-base amd64 1.23.0-7 [1185 kB] Get:31 http://localhost:9999/debian unstable/main amd64 bsdextrautils amd64 2.40.4-1 [92.2 kB] Get:32 http://localhost:9999/debian unstable/main amd64 libpipeline1 amd64 1.5.8-1 [42.0 kB] Get:33 http://localhost:9999/debian unstable/main amd64 man-db amd64 2.13.0-1 [1420 kB] Get:34 http://localhost:9999/debian unstable/main amd64 m4 amd64 1.4.19-5 [294 kB] Get:35 http://localhost:9999/debian unstable/main amd64 autoconf all 2.72-3 [493 kB] Get:36 http://localhost:9999/debian unstable/main amd64 autotools-dev all 20220109.1 [51.6 kB] Get:37 http://localhost:9999/debian unstable/main amd64 automake all 1:1.16.5-1.3 [823 kB] Get:38 http://localhost:9999/debian unstable/main amd64 autopoint all 0.22.5-4 [723 kB] Get:39 http://localhost:9999/debian unstable/main amd64 libncurses6 amd64 6.5-2+b1 [105 kB] Get:40 http://localhost:9999/debian unstable/main amd64 libncurses-dev amd64 6.5-2+b1 [351 kB] Get:41 http://localhost:9999/debian unstable/main amd64 libzstd-dev amd64 1.5.6+dfsg-2 [365 kB] Get:42 http://localhost:9999/debian unstable/main amd64 libdebhelper-perl all 13.23 [90.6 kB] Get:43 http://localhost:9999/debian unstable/main amd64 libtool all 2.5.4-2 [539 kB] Get:44 http://localhost:9999/debian unstable/main amd64 dh-autoreconf all 20 [17.1 kB] Get:45 http://localhost:9999/debian unstable/main amd64 libarchive-zip-perl all 1.68-1 [104 kB] Get:46 http://localhost:9999/debian unstable/main amd64 libfile-stripnondeterminism-perl all 1.14.0-1 [19.5 kB] Get:47 http://localhost:9999/debian unstable/main amd64 dh-strip-nondeterminism all 1.14.0-1 [8448 B] Get:48 http://localhost:9999/debian unstable/main amd64 libelf1t64 amd64 0.192-4 [189 kB] Get:49 http://localhost:9999/debian unstable/main amd64 dwz amd64 0.15-1+b1 [110 kB] Get:50 http://localhost:9999/debian unstable/main amd64 libunistring5 amd64 1.3-1 [476 kB] Get:51 http://localhost:9999/debian unstable/main amd64 libicu72 amd64 72.1-6 [9421 kB] Get:52 http://localhost:9999/debian unstable/main amd64 libxml2 amd64 2.12.7+dfsg+really2.9.14-0.2+b1 [699 kB] Get:53 file:/rebuilt ./ libstdlib-ocaml-dev 5.3.0-1~exp2+ocaml1 [7889 kB] Get:54 http://localhost:9999/debian unstable/main amd64 gettext amd64 0.22.5-4 [1600 kB] Get:55 http://localhost:9999/debian unstable/main amd64 intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get:56 http://localhost:9999/debian unstable/main amd64 po-debconf all 1.0.21+nmu1 [248 kB] Get:57 http://localhost:9999/debian unstable/main amd64 debhelper all 13.23 [919 kB] Get:58 http://localhost:9999/debian unstable/main amd64 libconfig-tiny-perl all 2.30-1 [18.9 kB] Get:59 http://localhost:9999/debian unstable/main amd64 libfakeroot amd64 1.36.2-1 [29.6 kB] Get:60 http://localhost:9999/debian unstable/main amd64 fakeroot amd64 1.36.2-1 [75.4 kB] Get:61 http://localhost:9999/debian unstable/main amd64 libgmpxx4ldbl amd64 2:6.3.0+dfsg-3 [329 kB] Get:62 http://localhost:9999/debian unstable/main amd64 libgmp-dev amd64 2:6.3.0+dfsg-3 [642 kB] Get:63 http://localhost:9999/debian unstable/main amd64 libgmp3-dev amd64 2:6.3.0+dfsg-3 [322 kB] Get:64 file:/rebuilt ./ libcompiler-libs-ocaml-dev 5.3.0-1~exp2+ocaml1 [48.2 MB] Get:65 file:/rebuilt ./ ocaml-interp 5.3.0-1~exp2+ocaml1 [7105 kB] Get:66 file:/rebuilt ./ ocaml 5.3.0-1~exp2+ocaml1 [18.0 MB] Get:67 file:/rebuilt ./ ocaml-findlib 1.9.6-3+ocaml1 [581 kB] Get:68 file:/rebuilt ./ coq 8.20.0+dfsg-1+ocaml1 [70.1 MB] Get:69 file:/rebuilt ./ dh-coq 0.13+ocaml1 [7008 B] Get:70 file:/rebuilt ./ dh-ocaml 2.4+ocaml1 [63.0 kB] Get:71 file:/rebuilt ./ libfindlib-ocaml-dev 1.9.6-3+ocaml1 [153 kB] Get:72 file:/rebuilt ./ libzarith-ocaml-dev 1.14-1+ocaml1 [143 kB] Get:73 file:/rebuilt ./ libcoq-core-ocaml-dev 8.20.0+dfsg-1+ocaml1 [68.7 MB] Get:74 file:/rebuilt ./ libsexplib0-ocaml 0.17.0-1+ocaml1 [129 kB] Get:75 file:/rebuilt ./ libppx-deriving-ocaml 6.0.3-1+ocaml1 [4321 kB] Get:76 file:/rebuilt ./ libelpi-ocaml 2.0.5-1+ocaml1 [3858 kB] Get:77 file:/rebuilt ./ libmenhir-ocaml-dev 20240715+ds-1+ocaml1 [887 kB] Get:78 file:/rebuilt ./ libocaml-compiler-libs-ocaml-dev 0.17.0-1+ocaml1 [171 kB] Get:79 file:/rebuilt ./ libppx-derivers-ocaml-dev 1.2.1-4+ocaml1 [19.8 kB] Get:80 file:/rebuilt ./ libsexplib0-ocaml-dev 0.17.0-1+ocaml1 [354 kB] Get:81 file:/rebuilt ./ libppxlib-ocaml-dev 0.34.0-1+ocaml1 [25.1 MB] Get:82 file:/rebuilt ./ libppx-deriving-ocaml-dev 6.0.3-1+ocaml1 [1057 kB] Get:83 file:/rebuilt ./ libre-ocaml-dev 1.12.0+really1.11.0-1+ocaml1 [1287 kB] Get:84 file:/rebuilt ./ libelpi-ocaml-dev 2.0.5-1+ocaml1 [15.4 MB] Get:85 file:/rebuilt ./ libcoq-elpi 2.3.0-1+ocaml1 [11.8 MB] Get:86 file:/rebuilt ./ libcoq-hierarchy-builder 1.8.0-1+ocaml1 [549 kB] Get:87 file:/rebuilt ./ libcoq-mathcomp-ssreflect 2.3.0-1+ocaml1 [8305 kB] Get:88 file:/rebuilt ./ libcoq-mathcomp-fingroup 2.3.0-1+ocaml1 [2307 kB] Get:89 file:/rebuilt ./ libcoq-mathcomp-algebra 2.3.0-1+ocaml1 [12.2 MB] Preconfiguring packages ... Fetched 30.1 MB in 1s (34.5 MB/s) Selecting previously unselected package libpython3.13-minimal:amd64. (Reading database ... 11791 files and directories currently installed.) Preparing to unpack .../libpython3.13-minimal_3.13.1-3_amd64.deb ... Unpacking libpython3.13-minimal:amd64 (3.13.1-3) ... Selecting previously unselected package libexpat1:amd64. Preparing to unpack .../libexpat1_2.6.4-1_amd64.deb ... Unpacking libexpat1:amd64 (2.6.4-1) ... Selecting previously unselected package python3.13-minimal. Preparing to unpack .../python3.13-minimal_3.13.1-3_amd64.deb ... Unpacking python3.13-minimal (3.13.1-3) ... Setting up libpython3.13-minimal:amd64 (3.13.1-3) ... Setting up libexpat1:amd64 (2.6.4-1) ... Setting up python3.13-minimal (3.13.1-3) ... Selecting previously unselected package python3-minimal. (Reading database ... 12125 files and directories currently installed.) Preparing to unpack .../00-python3-minimal_3.13.1-2_amd64.deb ... Unpacking python3-minimal (3.13.1-2) ... Selecting previously unselected package media-types. Preparing to unpack .../01-media-types_10.1.0_all.deb ... Unpacking media-types (10.1.0) ... Selecting previously unselected package netbase. Preparing to unpack .../02-netbase_6.4_all.deb ... Unpacking netbase (6.4) ... Selecting previously unselected package tzdata. Preparing to unpack .../03-tzdata_2024b-6_all.deb ... Unpacking tzdata (2024b-6) ... Selecting previously unselected package libffi8:amd64. Preparing to unpack .../04-libffi8_3.4.6-1_amd64.deb ... Unpacking libffi8:amd64 (3.4.6-1) ... Selecting previously unselected package libncursesw6:amd64. Preparing to unpack .../05-libncursesw6_6.5-2+b1_amd64.deb ... Unpacking libncursesw6:amd64 (6.5-2+b1) ... Selecting previously unselected package readline-common. Preparing to unpack .../06-readline-common_8.2-6_all.deb ... Unpacking readline-common (8.2-6) ... Selecting previously unselected package libreadline8t64:amd64. Preparing to unpack .../07-libreadline8t64_8.2-6_amd64.deb ... Adding 'diversion of /lib/x86_64-linux-gnu/libhistory.so.8 to /lib/x86_64-linux-gnu/libhistory.so.8.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/x86_64-linux-gnu/libhistory.so.8.2 to /lib/x86_64-linux-gnu/libhistory.so.8.2.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/x86_64-linux-gnu/libreadline.so.8 to /lib/x86_64-linux-gnu/libreadline.so.8.usr-is-merged by libreadline8t64' Adding 'diversion of /lib/x86_64-linux-gnu/libreadline.so.8.2 to /lib/x86_64-linux-gnu/libreadline.so.8.2.usr-is-merged by libreadline8t64' Unpacking libreadline8t64:amd64 (8.2-6) ... Selecting previously unselected package libsqlite3-0:amd64. Preparing to unpack .../08-libsqlite3-0_3.46.1-1_amd64.deb ... Unpacking libsqlite3-0:amd64 (3.46.1-1) ... Selecting previously unselected package libpython3.13-stdlib:amd64. Preparing to unpack .../09-libpython3.13-stdlib_3.13.1-3_amd64.deb ... Unpacking libpython3.13-stdlib:amd64 (3.13.1-3) ... Selecting previously unselected package python3.13. Preparing to unpack .../10-python3.13_3.13.1-3_amd64.deb ... Unpacking python3.13 (3.13.1-3) ... Selecting previously unselected package libpython3-stdlib:amd64. Preparing to unpack .../11-libpython3-stdlib_3.13.1-2_amd64.deb ... Unpacking libpython3-stdlib:amd64 (3.13.1-2) ... Setting up python3-minimal (3.13.1-2) ... Selecting previously unselected package python3. (Reading database ... 13152 files and directories currently installed.) Preparing to unpack .../00-python3_3.13.1-2_amd64.deb ... Unpacking python3 (3.13.1-2) ... Selecting previously unselected package sensible-utils. Preparing to unpack .../01-sensible-utils_0.0.24_all.deb ... Unpacking sensible-utils (0.0.24) ... Selecting previously unselected package libmagic-mgc. Preparing to unpack .../02-libmagic-mgc_1%3a5.45-3+b1_amd64.deb ... Unpacking libmagic-mgc (1:5.45-3+b1) ... Selecting previously unselected package libmagic1t64:amd64. Preparing to unpack .../03-libmagic1t64_1%3a5.45-3+b1_amd64.deb ... Unpacking libmagic1t64:amd64 (1:5.45-3+b1) ... Selecting previously unselected package file. Preparing to unpack .../04-file_1%3a5.45-3+b1_amd64.deb ... Unpacking file (1:5.45-3+b1) ... Selecting previously unselected package gettext-base. Preparing to unpack .../05-gettext-base_0.22.5-4_amd64.deb ... Unpacking gettext-base (0.22.5-4) ... Selecting previously unselected package libuchardet0:amd64. Preparing to unpack .../06-libuchardet0_0.0.8-1+b2_amd64.deb ... Unpacking libuchardet0:amd64 (0.0.8-1+b2) ... Selecting previously unselected package groff-base. Preparing to unpack .../07-groff-base_1.23.0-7_amd64.deb ... Unpacking groff-base (1.23.0-7) ... Selecting previously unselected package bsdextrautils. Preparing to unpack .../08-bsdextrautils_2.40.4-1_amd64.deb ... Unpacking bsdextrautils (2.40.4-1) ... Selecting previously unselected package libpipeline1:amd64. Preparing to unpack .../09-libpipeline1_1.5.8-1_amd64.deb ... Unpacking libpipeline1:amd64 (1.5.8-1) ... Selecting previously unselected package man-db. Preparing to unpack .../10-man-db_2.13.0-1_amd64.deb ... Unpacking man-db (2.13.0-1) ... Selecting previously unselected package m4. Preparing to unpack .../11-m4_1.4.19-5_amd64.deb ... Unpacking m4 (1.4.19-5) ... Selecting previously unselected package autoconf. Preparing to unpack .../12-autoconf_2.72-3_all.deb ... Unpacking autoconf (2.72-3) ... Selecting previously unselected package autotools-dev. Preparing to unpack .../13-autotools-dev_20220109.1_all.deb ... Unpacking autotools-dev (20220109.1) ... Selecting previously unselected package automake. Preparing to unpack .../14-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 .../15-autopoint_0.22.5-4_all.deb ... Unpacking autopoint (0.22.5-4) ... Selecting previously unselected package libcoq-stdlib. Preparing to unpack .../16-libcoq-stdlib_8.20.0+dfsg-1+ocaml1_amd64.deb ... Unpacking libcoq-stdlib (8.20.0+dfsg-1+ocaml1) ... Selecting previously unselected package libstdlib-ocaml. Preparing to unpack .../17-libstdlib-ocaml_5.3.0-1~exp2+ocaml1_amd64.deb ... Unpacking libstdlib-ocaml (5.3.0-1~exp2+ocaml1) ... Selecting previously unselected package ocaml-base. Preparing to unpack .../18-ocaml-base_5.3.0-1~exp2+ocaml1_amd64.deb ... Unpacking ocaml-base (5.3.0-1~exp2+ocaml1) ... Selecting previously unselected package libfindlib-ocaml. Preparing to unpack .../19-libfindlib-ocaml_1.9.6-3+ocaml1_amd64.deb ... Unpacking libfindlib-ocaml (1.9.6-3+ocaml1) ... Selecting previously unselected package libzarith-ocaml. Preparing to unpack .../20-libzarith-ocaml_1.14-1+ocaml1_amd64.deb ... Unpacking libzarith-ocaml (1.14-1+ocaml1) ... Selecting previously unselected package libcoq-core-ocaml. Preparing to unpack .../21-libcoq-core-ocaml_8.20.0+dfsg-1+ocaml1_amd64.deb ... Unpacking libcoq-core-ocaml (8.20.0+dfsg-1+ocaml1) ... Selecting previously unselected package libstdlib-ocaml-dev. Preparing to unpack .../22-libstdlib-ocaml-dev_5.3.0-1~exp2+ocaml1_amd64.deb ... Unpacking libstdlib-ocaml-dev (5.3.0-1~exp2+ocaml1) ... Selecting previously unselected package libcompiler-libs-ocaml-dev. Preparing to unpack .../23-libcompiler-libs-ocaml-dev_5.3.0-1~exp2+ocaml1_amd64.deb ... Unpacking libcompiler-libs-ocaml-dev (5.3.0-1~exp2+ocaml1) ... Selecting previously unselected package ocaml-interp. Preparing to unpack .../24-ocaml-interp_5.3.0-1~exp2+ocaml1_amd64.deb ... Unpacking ocaml-interp (5.3.0-1~exp2+ocaml1) ... Selecting previously unselected package libncurses6:amd64. Preparing to unpack .../25-libncurses6_6.5-2+b1_amd64.deb ... Unpacking libncurses6:amd64 (6.5-2+b1) ... Selecting previously unselected package libncurses-dev:amd64. Preparing to unpack .../26-libncurses-dev_6.5-2+b1_amd64.deb ... Unpacking libncurses-dev:amd64 (6.5-2+b1) ... Selecting previously unselected package libzstd-dev:amd64. Preparing to unpack .../27-libzstd-dev_1.5.6+dfsg-2_amd64.deb ... Unpacking libzstd-dev:amd64 (1.5.6+dfsg-2) ... Selecting previously unselected package ocaml. Preparing to unpack .../28-ocaml_5.3.0-1~exp2+ocaml1_amd64.deb ... Unpacking ocaml (5.3.0-1~exp2+ocaml1) ... Selecting previously unselected package ocaml-findlib. Preparing to unpack .../29-ocaml-findlib_1.9.6-3+ocaml1_amd64.deb ... Unpacking ocaml-findlib (1.9.6-3+ocaml1) ... Selecting previously unselected package coq. Preparing to unpack .../30-coq_8.20.0+dfsg-1+ocaml1_amd64.deb ... Unpacking coq (8.20.0+dfsg-1+ocaml1) ... Selecting previously unselected package libdebhelper-perl. Preparing to unpack .../31-libdebhelper-perl_13.23_all.deb ... Unpacking libdebhelper-perl (13.23) ... Selecting previously unselected package libtool. Preparing to unpack .../32-libtool_2.5.4-2_all.deb ... Unpacking libtool (2.5.4-2) ... Selecting previously unselected package dh-autoreconf. Preparing to unpack .../33-dh-autoreconf_20_all.deb ... Unpacking dh-autoreconf (20) ... Selecting previously unselected package libarchive-zip-perl. Preparing to unpack .../34-libarchive-zip-perl_1.68-1_all.deb ... Unpacking libarchive-zip-perl (1.68-1) ... Selecting previously unselected package libfile-stripnondeterminism-perl. Preparing to unpack .../35-libfile-stripnondeterminism-perl_1.14.0-1_all.deb ... Unpacking libfile-stripnondeterminism-perl (1.14.0-1) ... Selecting previously unselected package dh-strip-nondeterminism. Preparing to unpack .../36-dh-strip-nondeterminism_1.14.0-1_all.deb ... Unpacking dh-strip-nondeterminism (1.14.0-1) ... Selecting previously unselected package libelf1t64:amd64. Preparing to unpack .../37-libelf1t64_0.192-4_amd64.deb ... Unpacking libelf1t64:amd64 (0.192-4) ... Selecting previously unselected package dwz. Preparing to unpack .../38-dwz_0.15-1+b1_amd64.deb ... Unpacking dwz (0.15-1+b1) ... Selecting previously unselected package libunistring5:amd64. Preparing to unpack .../39-libunistring5_1.3-1_amd64.deb ... Unpacking libunistring5:amd64 (1.3-1) ... Selecting previously unselected package libicu72:amd64. Preparing to unpack .../40-libicu72_72.1-6_amd64.deb ... Unpacking libicu72:amd64 (72.1-6) ... Selecting previously unselected package libxml2:amd64. Preparing to unpack .../41-libxml2_2.12.7+dfsg+really2.9.14-0.2+b1_amd64.deb ... Unpacking libxml2:amd64 (2.12.7+dfsg+really2.9.14-0.2+b1) ... Selecting previously unselected package gettext. Preparing to unpack .../42-gettext_0.22.5-4_amd64.deb ... Unpacking gettext (0.22.5-4) ... 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.23_all.deb ... Unpacking debhelper (13.23) ... Selecting previously unselected package dh-coq. Preparing to unpack .../46-dh-coq_0.13+ocaml1_all.deb ... Unpacking dh-coq (0.13+ocaml1) ... Selecting previously unselected package libconfig-tiny-perl. Preparing to unpack .../47-libconfig-tiny-perl_2.30-1_all.deb ... Unpacking libconfig-tiny-perl (2.30-1) ... Selecting previously unselected package dh-ocaml. Preparing to unpack .../48-dh-ocaml_2.4+ocaml1_all.deb ... Unpacking dh-ocaml (2.4+ocaml1) ... Selecting previously unselected package libfakeroot:amd64. Preparing to unpack .../49-libfakeroot_1.36.2-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.36.2-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../50-fakeroot_1.36.2-1_amd64.deb ... Unpacking fakeroot (1.36.2-1) ... Selecting previously unselected package libfindlib-ocaml-dev. Preparing to unpack .../51-libfindlib-ocaml-dev_1.9.6-3+ocaml1_amd64.deb ... Unpacking libfindlib-ocaml-dev (1.9.6-3+ocaml1) ... Selecting previously unselected package libgmpxx4ldbl:amd64. Preparing to unpack .../52-libgmpxx4ldbl_2%3a6.3.0+dfsg-3_amd64.deb ... Unpacking libgmpxx4ldbl:amd64 (2:6.3.0+dfsg-3) ... Selecting previously unselected package libgmp-dev:amd64. Preparing to unpack .../53-libgmp-dev_2%3a6.3.0+dfsg-3_amd64.deb ... Unpacking libgmp-dev:amd64 (2:6.3.0+dfsg-3) ... Selecting previously unselected package libgmp3-dev:amd64. Preparing to unpack .../54-libgmp3-dev_2%3a6.3.0+dfsg-3_amd64.deb ... Unpacking libgmp3-dev:amd64 (2:6.3.0+dfsg-3) ... Selecting previously unselected package libzarith-ocaml-dev. Preparing to unpack .../55-libzarith-ocaml-dev_1.14-1+ocaml1_amd64.deb ... Unpacking libzarith-ocaml-dev (1.14-1+ocaml1) ... Selecting previously unselected package libcoq-core-ocaml-dev. Preparing to unpack .../56-libcoq-core-ocaml-dev_8.20.0+dfsg-1+ocaml1_amd64.deb ... Unpacking libcoq-core-ocaml-dev (8.20.0+dfsg-1+ocaml1) ... Selecting previously unselected package libsexplib0-ocaml. Preparing to unpack .../57-libsexplib0-ocaml_0.17.0-1+ocaml1_amd64.deb ... Unpacking libsexplib0-ocaml (0.17.0-1+ocaml1) ... Selecting previously unselected package libppx-deriving-ocaml. Preparing to unpack .../58-libppx-deriving-ocaml_6.0.3-1+ocaml1_amd64.deb ... Unpacking libppx-deriving-ocaml (6.0.3-1+ocaml1) ... Selecting previously unselected package libelpi-ocaml. Preparing to unpack .../59-libelpi-ocaml_2.0.5-1+ocaml1_amd64.deb ... Unpacking libelpi-ocaml (2.0.5-1+ocaml1) ... Selecting previously unselected package libmenhir-ocaml-dev. Preparing to unpack .../60-libmenhir-ocaml-dev_20240715+ds-1+ocaml1_amd64.deb ... Unpacking libmenhir-ocaml-dev (20240715+ds-1+ocaml1) ... Selecting previously unselected package libocaml-compiler-libs-ocaml-dev. Preparing to unpack .../61-libocaml-compiler-libs-ocaml-dev_0.17.0-1+ocaml1_amd64.deb ... Unpacking libocaml-compiler-libs-ocaml-dev (0.17.0-1+ocaml1) ... Selecting previously unselected package libppx-derivers-ocaml-dev. Preparing to unpack .../62-libppx-derivers-ocaml-dev_1.2.1-4+ocaml1_amd64.deb ... Unpacking libppx-derivers-ocaml-dev (1.2.1-4+ocaml1) ... Selecting previously unselected package libsexplib0-ocaml-dev. Preparing to unpack .../63-libsexplib0-ocaml-dev_0.17.0-1+ocaml1_amd64.deb ... Unpacking libsexplib0-ocaml-dev (0.17.0-1+ocaml1) ... Selecting previously unselected package libppxlib-ocaml-dev. Preparing to unpack .../64-libppxlib-ocaml-dev_0.34.0-1+ocaml1_amd64.deb ... Unpacking libppxlib-ocaml-dev (0.34.0-1+ocaml1) ... Selecting previously unselected package libppx-deriving-ocaml-dev. Preparing to unpack .../65-libppx-deriving-ocaml-dev_6.0.3-1+ocaml1_amd64.deb ... Unpacking libppx-deriving-ocaml-dev (6.0.3-1+ocaml1) ... Selecting previously unselected package libre-ocaml-dev. Preparing to unpack .../66-libre-ocaml-dev_1.12.0+really1.11.0-1+ocaml1_amd64.deb ... Unpacking libre-ocaml-dev (1.12.0+really1.11.0-1+ocaml1) ... Selecting previously unselected package libelpi-ocaml-dev. Preparing to unpack .../67-libelpi-ocaml-dev_2.0.5-1+ocaml1_amd64.deb ... Unpacking libelpi-ocaml-dev (2.0.5-1+ocaml1) ... Selecting previously unselected package libcoq-elpi. Preparing to unpack .../68-libcoq-elpi_2.3.0-1+ocaml1_amd64.deb ... Unpacking libcoq-elpi (2.3.0-1+ocaml1) ... Selecting previously unselected package libcoq-hierarchy-builder. Preparing to unpack .../69-libcoq-hierarchy-builder_1.8.0-1+ocaml1_amd64.deb ... Unpacking libcoq-hierarchy-builder (1.8.0-1+ocaml1) ... Selecting previously unselected package libcoq-mathcomp-ssreflect. Preparing to unpack .../70-libcoq-mathcomp-ssreflect_2.3.0-1+ocaml1_amd64.deb ... Unpacking libcoq-mathcomp-ssreflect (2.3.0-1+ocaml1) ... Selecting previously unselected package libcoq-mathcomp-fingroup. Preparing to unpack .../71-libcoq-mathcomp-fingroup_2.3.0-1+ocaml1_amd64.deb ... Unpacking libcoq-mathcomp-fingroup (2.3.0-1+ocaml1) ... Selecting previously unselected package libcoq-mathcomp-algebra. Preparing to unpack .../72-libcoq-mathcomp-algebra_2.3.0-1+ocaml1_amd64.deb ... Unpacking libcoq-mathcomp-algebra (2.3.0-1+ocaml1) ... Selecting previously unselected package sbuild-build-depends-main-dummy. Preparing to unpack .../73-sbuild-build-depends-main-dummy_0.invalid.0_amd64.deb ... Unpacking sbuild-build-depends-main-dummy (0.invalid.0) ... Setting up media-types (10.1.0) ... Setting up libpipeline1:amd64 (1.5.8-1) ... Setting up libicu72:amd64 (72.1-6) ... Setting up libzstd-dev:amd64 (1.5.6+dfsg-2) ... Setting up bsdextrautils (2.40.4-1) ... Setting up libmagic-mgc (1:5.45-3+b1) ... Setting up dh-coq (0.13+ocaml1) ... Setting up libarchive-zip-perl (1.68-1) ... Setting up libdebhelper-perl (13.23) ... Setting up libsqlite3-0:amd64 (3.46.1-1) ... Setting up libmagic1t64:amd64 (1:5.45-3+b1) ... Setting up gettext-base (0.22.5-4) ... Setting up m4 (1.4.19-5) ... Setting up file (1:5.45-3+b1) ... Setting up libconfig-tiny-perl (2.30-1) ... Setting up libfakeroot:amd64 (1.36.2-1) ... Setting up libelf1t64:amd64 (0.192-4) ... Setting up tzdata (2024b-6) ... Current default time zone: 'Etc/UTC' Local time is now: Wed Jan 15 15:52:15 UTC 2025. Universal Time is now: Wed Jan 15 15:52:15 UTC 2025. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up fakeroot (1.36.2-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Setting up autotools-dev (20220109.1) ... Setting up libcoq-stdlib (8.20.0+dfsg-1+ocaml1) ... Setting up libgmpxx4ldbl:amd64 (2:6.3.0+dfsg-3) ... Setting up libncurses6:amd64 (6.5-2+b1) ... Setting up libstdlib-ocaml (5.3.0-1~exp2+ocaml1) ... Setting up libunistring5:amd64 (1.3-1) ... Setting up autopoint (0.22.5-4) ... Setting up ocaml-base (5.3.0-1~exp2+ocaml1) ... Setting up libncursesw6:amd64 (6.5-2+b1) ... Setting up autoconf (2.72-3) ... Setting up libffi8:amd64 (3.4.6-1) ... Setting up libsexplib0-ocaml (0.17.0-1+ocaml1) ... Setting up dwz (0.15-1+b1) ... Setting up sensible-utils (0.0.24) ... Setting up libuchardet0:amd64 (0.0.8-1+b2) ... Setting up netbase (6.4) ... Setting up readline-common (8.2-6) ... Setting up libxml2:amd64 (2.12.7+dfsg+really2.9.14-0.2+b1) ... 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.14.0-1) ... Setting up libppx-deriving-ocaml (6.0.3-1+ocaml1) ... Setting up libncurses-dev:amd64 (6.5-2+b1) ... Setting up gettext (0.22.5-4) ... Setting up libgmp-dev:amd64 (2:6.3.0+dfsg-3) ... Setting up libtool (2.5.4-2) ... Setting up libstdlib-ocaml-dev (5.3.0-1~exp2+ocaml1) ... Setting up dh-ocaml (2.4+ocaml1) ... Setting up libfindlib-ocaml (1.9.6-3+ocaml1) ... Setting up libzarith-ocaml (1.14-1+ocaml1) ... Setting up intltool-debian (0.35.0+20060710.6) ... Setting up dh-autoreconf (20) ... Setting up libcompiler-libs-ocaml-dev (5.3.0-1~exp2+ocaml1) ... Setting up ocaml-interp (5.3.0-1~exp2+ocaml1) ... Setting up ocaml-findlib (1.9.6-3+ocaml1) ... Setting up libreadline8t64:amd64 (8.2-6) ... Setting up dh-strip-nondeterminism (1.14.0-1) ... Setting up libelpi-ocaml (2.0.5-1+ocaml1) ... Setting up libcoq-core-ocaml (8.20.0+dfsg-1+ocaml1) ... Setting up groff-base (1.23.0-7) ... Setting up libgmp3-dev:amd64 (2:6.3.0+dfsg-3) ... Setting up libpython3.13-stdlib:amd64 (3.13.1-3) ... Setting up libpython3-stdlib:amd64 (3.13.1-2) ... Setting up python3.13 (3.13.1-3) ... Setting up po-debconf (1.0.21+nmu1) ... Setting up python3 (3.13.1-2) ... Setting up ocaml (5.3.0-1~exp2+ocaml1) ... Setting up man-db (2.13.0-1) ... Not building database; man-db/auto-update is not 'true'. Setting up libre-ocaml-dev (1.12.0+really1.11.0-1+ocaml1) ... Setting up libmenhir-ocaml-dev (20240715+ds-1+ocaml1) ... Setting up libocaml-compiler-libs-ocaml-dev (0.17.0-1+ocaml1) ... Setting up libfindlib-ocaml-dev (1.9.6-3+ocaml1) ... Setting up libsexplib0-ocaml-dev (0.17.0-1+ocaml1) ... Setting up coq (8.20.0+dfsg-1+ocaml1) ... Setting up libzarith-ocaml-dev (1.14-1+ocaml1) ... Setting up libppx-derivers-ocaml-dev (1.2.1-4+ocaml1) ... Setting up libppxlib-ocaml-dev (0.34.0-1+ocaml1) ... Setting up debhelper (13.23) ... Setting up libcoq-core-ocaml-dev (8.20.0+dfsg-1+ocaml1) ... Setting up libppx-deriving-ocaml-dev (6.0.3-1+ocaml1) ... Setting up libelpi-ocaml-dev (2.0.5-1+ocaml1) ... Setting up libcoq-elpi (2.3.0-1+ocaml1) ... Setting up libcoq-hierarchy-builder (1.8.0-1+ocaml1) ... Setting up libcoq-mathcomp-ssreflect (2.3.0-1+ocaml1) ... Setting up libcoq-mathcomp-fingroup (2.3.0-1+ocaml1) ... Setting up libcoq-mathcomp-algebra (2.3.0-1+ocaml1) ... Setting up sbuild-build-depends-main-dummy (0.invalid.0) ... Processing triggers for libc-bin (2.40-5) ... +------------------------------------------------------------------------------+ | Check architectures Wed, 15 Jan 2025 15:52:17 +0000 | +------------------------------------------------------------------------------+ Arch check ok (amd64 included in any) +------------------------------------------------------------------------------+ | Build environment Wed, 15 Jan 2025 15:52:17 +0000 | +------------------------------------------------------------------------------+ Kernel: Linux 6.12.6-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.6-1 (2024-12-21) amd64 (x86_64) Toolchain package versions: binutils_2.43.50.20250108-1 dpkg-dev_1.22.13 g++-14_14.2.0-13 gcc-14_14.2.0-13 libc6-dev_2.40-5 libstdc++-14-dev_14.2.0-13 libstdc++6_14.2.0-13 linux-libc-dev_6.12.9-1 Package versions: apt_2.9.22 autoconf_2.72-3 automake_1:1.16.5-1.3 autopoint_0.22.5-4 autotools-dev_20220109.1 base-files_13.6 base-passwd_3.6.6 bash_5.2.37-1 binutils_2.43.50.20250108-1 binutils-common_2.43.50.20250108-1 binutils-x86-64-linux-gnu_2.43.50.20250108-1 bsdextrautils_2.40.4-1 bsdutils_1:2.40.4-1 build-essential_12.12 bzip2_1.0.8-6 coq_8.20.0+dfsg-1+ocaml1 coreutils_9.5-1+b1 cpp_4:14.2.0-1 cpp-14_14.2.0-13 cpp-14-x86-64-linux-gnu_14.2.0-13 cpp-x86-64-linux-gnu_4:14.2.0-1 dash_0.5.12-11 debconf_1.5.89 debhelper_13.23 debian-archive-keyring_2023.4 debianutils_5.21 dh-autoreconf_20 dh-coq_0.13+ocaml1 dh-ocaml_2.4+ocaml1 dh-strip-nondeterminism_1.14.0-1 diffutils_1:3.10-2 dpkg_1.22.13 dpkg-dev_1.22.13 dwz_0.15-1+b1 fakeroot_1.36.2-1 file_1:5.45-3+b1 findutils_4.10.0-3 g++_4:14.2.0-1 g++-14_14.2.0-13 g++-14-x86-64-linux-gnu_14.2.0-13 g++-x86-64-linux-gnu_4:14.2.0-1 gcc_4:14.2.0-1 gcc-14_14.2.0-13 gcc-14-base_14.2.0-13 gcc-14-x86-64-linux-gnu_14.2.0-13 gcc-x86-64-linux-gnu_4:14.2.0-1 gettext_0.22.5-4 gettext-base_0.22.5-4 grep_3.11-4 groff-base_1.23.0-7 gzip_1.12-1.2 hostname_3.25 init-system-helpers_1.68 intltool-debian_0.35.0+20060710.6 libacl1_2.3.2-2+b1 libapt-pkg6.0t64_2.9.22 libarchive-zip-perl_1.68-1 libasan8_14.2.0-13 libatomic1_14.2.0-13 libattr1_1:2.5.2-2 libaudit-common_1:4.0.2-2 libaudit1_1:4.0.2-2 libbinutils_2.43.50.20250108-1 libblkid1_2.40.4-1 libbz2-1.0_1.0.8-6 libc-bin_2.40-5 libc-dev-bin_2.40-5 libc6_2.40-5 libc6-dev_2.40-5 libcap-ng0_0.8.5-4 libcap2_1:2.66-5+b1 libcc1-0_14.2.0-13 libcompiler-libs-ocaml-dev_5.3.0-1~exp2+ocaml1 libconfig-tiny-perl_2.30-1 libcoq-core-ocaml_8.20.0+dfsg-1+ocaml1 libcoq-core-ocaml-dev_8.20.0+dfsg-1+ocaml1 libcoq-elpi_2.3.0-1+ocaml1 libcoq-hierarchy-builder_1.8.0-1+ocaml1 libcoq-mathcomp-algebra_2.3.0-1+ocaml1 libcoq-mathcomp-fingroup_2.3.0-1+ocaml1 libcoq-mathcomp-ssreflect_2.3.0-1+ocaml1 libcoq-stdlib_8.20.0+dfsg-1+ocaml1 libcrypt-dev_1:4.4.36-5 libcrypt1_1:4.4.36-5 libctf-nobfd0_2.43.50.20250108-1 libctf0_2.43.50.20250108-1 libdb5.3t64_5.3.28+dfsg2-9 libdebconfclient0_0.277 libdebhelper-perl_13.23 libdpkg-perl_1.22.13 libelf1t64_0.192-4 libelpi-ocaml_2.0.5-1+ocaml1 libelpi-ocaml-dev_2.0.5-1+ocaml1 libexpat1_2.6.4-1 libfakeroot_1.36.2-1 libffi8_3.4.6-1 libfile-stripnondeterminism-perl_1.14.0-1 libfindlib-ocaml_1.9.6-3+ocaml1 libfindlib-ocaml-dev_1.9.6-3+ocaml1 libgcc-14-dev_14.2.0-13 libgcc-s1_14.2.0-13 libgdbm-compat4t64_1.24-2 libgdbm6t64_1.24-2 libgmp-dev_2:6.3.0+dfsg-3 libgmp10_2:6.3.0+dfsg-3 libgmp3-dev_2:6.3.0+dfsg-3 libgmpxx4ldbl_2:6.3.0+dfsg-3 libgomp1_14.2.0-13 libgprofng0_2.43.50.20250108-1 libhogweed6t64_3.10-1+b1 libhwasan0_14.2.0-13 libicu72_72.1-6 libisl23_0.27-1 libitm1_14.2.0-13 libjansson4_2.14-2+b3 liblsan0_14.2.0-13 liblz4-1_1.9.4-4 liblzma5_5.6.3-1+b1 libmagic-mgc_1:5.45-3+b1 libmagic1t64_1:5.45-3+b1 libmd0_1.1.0-2+b1 libmenhir-ocaml-dev_20240715+ds-1+ocaml1 libmount1_2.40.4-1 libmpc3_1.3.1-1+b3 libmpfr6_4.2.1-1+b2 libncurses-dev_6.5-2+b1 libncurses6_6.5-2+b1 libncursesw6_6.5-2+b1 libnettle8t64_3.10-1+b1 libocaml-compiler-libs-ocaml-dev_0.17.0-1+ocaml1 libpam-modules_1.5.3-7+b1 libpam-modules-bin_1.5.3-7+b1 libpam-runtime_1.5.3-7 libpam0g_1.5.3-7+b1 libpcre2-8-0_10.44-5 libperl5.40_5.40.0-8 libpipeline1_1.5.8-1 libppx-derivers-ocaml-dev_1.2.1-4+ocaml1 libppx-deriving-ocaml_6.0.3-1+ocaml1 libppx-deriving-ocaml-dev_6.0.3-1+ocaml1 libppxlib-ocaml-dev_0.34.0-1+ocaml1 libpython3-stdlib_3.13.1-2 libpython3.13-minimal_3.13.1-3 libpython3.13-stdlib_3.13.1-3 libquadmath0_14.2.0-13 libre-ocaml-dev_1.12.0+really1.11.0-1+ocaml1 libreadline8t64_8.2-6 libseccomp2_2.5.5-2 libselinux1_3.7-3+b1 libsexplib0-ocaml_0.17.0-1+ocaml1 libsexplib0-ocaml-dev_0.17.0-1+ocaml1 libsframe1_2.43.50.20250108-1 libsmartcols1_2.40.4-1 libsqlite3-0_3.46.1-1 libssl3t64_3.4.0-2 libstdc++-14-dev_14.2.0-13 libstdc++6_14.2.0-13 libstdlib-ocaml_5.3.0-1~exp2+ocaml1 libstdlib-ocaml-dev_5.3.0-1~exp2+ocaml1 libsystemd0_257.2-1 libtinfo6_6.5-2+b1 libtool_2.5.4-2 libtsan2_14.2.0-13 libubsan1_14.2.0-13 libuchardet0_0.0.8-1+b2 libudev1_257.2-1 libunistring5_1.3-1 libuuid1_2.40.4-1 libxml2_2.12.7+dfsg+really2.9.14-0.2+b1 libxxhash0_0.8.3-2 libzarith-ocaml_1.14-1+ocaml1 libzarith-ocaml-dev_1.14-1+ocaml1 libzstd-dev_1.5.6+dfsg-2 libzstd1_1.5.6+dfsg-2 linux-libc-dev_6.12.9-1 m4_1.4.19-5 make_4.4.1-1 man-db_2.13.0-1 mawk_1.3.4.20240905-1 media-types_10.1.0 ncurses-base_6.5-2 ncurses-bin_6.5-2+b1 netbase_6.4 ocaml_5.3.0-1~exp2+ocaml1 ocaml-base_5.3.0-1~exp2+ocaml1 ocaml-findlib_1.9.6-3+ocaml1 ocaml-interp_5.3.0-1~exp2+ocaml1 openssl-provider-legacy_3.4.0-2 patch_2.7.6-7 perl_5.40.0-8 perl-base_5.40.0-8 perl-modules-5.40_5.40.0-8 po-debconf_1.0.21+nmu1 python3_3.13.1-2 python3-minimal_3.13.1-2 python3.13_3.13.1-3 python3.13-minimal_3.13.1-3 readline-common_8.2-6 rpcsvc-proto_1.4.3-1 sbuild-build-depends-main-dummy_0.invalid.0 sed_4.9-2 sensible-utils_0.0.24 sqv_1.2.1-5 sysvinit-utils_3.13-1 tar_1.35+dfsg-3.1 tzdata_2024b-6 util-linux_2.40.4-1 xz-utils_5.6.3-1+b1 zlib1g_1:1.3.dfsg+really1.3.1-1+b1 +------------------------------------------------------------------------------+ | Build Wed, 15 Jan 2025 15:52:17 +0000 | +------------------------------------------------------------------------------+ Unpack source ------------- Format: 3.0 (quilt) Source: mathcomp-zify Binary: libcoq-mathcomp-zify Architecture: any Version: 1.5.0+2.0+8.16-4+ocaml1 Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Homepage: https://github.com/math-comp/mczify Standards-Version: 4.7.0 Vcs-Browser: https://salsa.debian.org/ocaml-team/mathcomp-zify Vcs-Git: https://salsa.debian.org/ocaml-team/mathcomp-zify.git Testsuite: autopkgtest Testsuite-Triggers: coq Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-mathcomp-algebra Package-List: libcoq-mathcomp-zify deb ocaml optional arch=any Checksums-Sha1: cb3d53e9c1680fb90be08563bc6c0f14ce4779a2 21080 mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz 105f323a4284df7479fb01e22eb650f376290f9b 8832 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz Checksums-Sha256: 5988389c6c8dfde4d2f3a370278c6b2aa1b5a0f56531cb30b0cce2d550b4387c 21080 mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz c7d2e8b1454121a009fd4b5af403b5c5a478ad22cdf69670c9222c1b017cac8e 8832 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz Files: c9d02b943ba8148a27ec3e02a21bdcf2 21080 mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz df578717b89ef39606a7043da5cb7702 8832 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz dpkg-source: warning: extracting unsigned source package (mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc) dpkg-source: info: extracting mathcomp-zify in /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16 dpkg-source: info: unpacking mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz dpkg-source: info: unpacking mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz Check disk space ---------------- Sufficient free space for build User Environment ---------------- APT_CONFIG=/var/lib/sbuild/apt.conf DEB_BUILD_OPTIONS=parallel=1 HOME=/sbuild-nonexistent LANG=fr_FR.UTF-8 LC_ALL=C.UTF-8 LOGNAME=steph MAKEFLAGS= PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games SHELL=/bin/sh USER=steph dpkg-buildpackage ----------------- Command: dpkg-buildpackage --sanitize-env -us -uc -sa dpkg-buildpackage: info: source package mathcomp-zify dpkg-buildpackage: info: source version 1.5.0+2.0+8.16-4+ocaml1 dpkg-buildpackage: info: source distribution unstable-ocaml dpkg-buildpackage: info: source changed by Anonymous Builder dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with coq,ocaml dh_auto_clean make -j1 distclean make[1]: Entering directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' rm -f Makefile.coq Makefile.coq.conf rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf make[1]: Leaving directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' dh_ocamlclean dh_clean dpkg-source -b . dpkg-source: info: using source format '3.0 (quilt)' dpkg-source: info: building mathcomp-zify using existing ./mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz dpkg-source: info: building mathcomp-zify in mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz dpkg-source: info: building mathcomp-zify in mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc debian/rules binary dh binary --with coq,ocaml dh_update_autotools_config dh_autoreconf dh_ocamlinit dh_auto_configure debian/rules override_dh_auto_build make[1]: Entering directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' make make[2]: Entering directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' coq_makefile -f Make -o Makefile.coq make --no-print-directory -f Makefile.coq COQDEP VFILES COQC theories/zify_ssreflect.v File "./theories/zify_ssreflect.v", line 157, characters 29-37: Warning: Reference addn_rec is deprecated since mathcomp 2.3.0. Use addn instead. [deprecated-reference-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-reference,deprecated,default] File "./theories/zify_ssreflect.v", line 170, characters 29-37: Warning: Reference subn_rec is deprecated since mathcomp 2.3.0. Use subn instead. [deprecated-reference-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-reference,deprecated,default] File "./theories/zify_ssreflect.v", line 178, characters 29-37: Warning: Reference muln_rec is deprecated since mathcomp 2.3.0. Use muln instead. [deprecated-reference-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-reference,deprecated,default] File "./theories/zify_ssreflect.v", line 239, characters 29-37: Warning: Reference expn_rec is deprecated since mathcomp 2.3.0. Use expn instead. [deprecated-reference-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-reference,deprecated,default] COQC theories/ssrZ.v File "./theories/ssrZ.v", line 6, characters 0-74: Warning: New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed. [ambiguous-paths,coercions,default] File "./theories/ssrZ.v", line 6, characters 0-74: Warning: New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed. New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed. [ambiguous-paths,coercions,default] File "./theories/ssrZ.v", line 6, characters 0-74: Warning: New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed. [ambiguous-paths,coercions,default] File "./theories/ssrZ.v", line 6, characters 0-74: Warning: New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed. [ambiguous-paths,coercions,default] File "./theories/ssrZ.v", line 6, characters 0-74: Warning: New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed. [ambiguous-paths,coercions,default] File "./theories/ssrZ.v", line 6, characters 0-74: Warning: New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed. [ambiguous-paths,coercions,default] File "./theories/ssrZ.v", line 42, characters 0-82: Warning: Ignoring canonical projection to add0n by GRing.isNmodule.add0r in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 42, characters 0-82: Warning: Ignoring canonical projection to addnC by GRing.isNmodule.addrC in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 42, characters 0-82: Warning: Ignoring canonical projection to addnA by GRing.isNmodule.addrA in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 42, characters 0-82: Warning: Ignoring canonical projection to addn by GRing.isNmodule.add in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 42, characters 0-82: Warning: Ignoring canonical projection to O by GRing.isNmodule.zero in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrC by GRing.SemiRing_hasCommutativeMul.mulrC in HB_unnamed_mixin_822: redundant with GRing_Nmodule_isComSemiRing__to__GRing_SemiRing_hasCommutativeMul [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.oner_neq0 by GRing.Nmodule_isSemiRing.oner_neq0 in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Builders_211.mulr0 by GRing.Nmodule_isSemiRing.mulr0 in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul0r by GRing.Nmodule_isSemiRing.mul0r in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Builders_211.mulrDr by GRing.Nmodule_isSemiRing.mulrDr in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrDl by GRing.Nmodule_isSemiRing.mulrDl in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Builders_211.mulr1 by GRing.Nmodule_isSemiRing.mulr1 in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul1r by GRing.Nmodule_isSemiRing.mul1r in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrA by GRing.Nmodule_isSemiRing.mulrA in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul by GRing.Nmodule_isSemiRing.mul in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.one by GRing.Nmodule_isSemiRing.one in HB_unnamed_mixin_821: redundant with GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 45, characters 0-115: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/ssrZ.v", line 49, characters 0-135: Warning: Ignoring canonical projection to pair by GRing.isSemiAdditive.semi_additive_subproof in GRing_isSemiAdditive__to__GRing_isSemiAdditive: redundant with HB_unnamed_factory_824 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 49, characters 0-135: Warning: Ignoring canonical projection to pair by GRing.isSemiAdditive.semi_additive_subproof in GRing_isSemiAdditive__to__GRing_isSemiAdditive: redundant with HB_unnamed_factory_824 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 53, characters 0-131: Warning: Ignoring canonical projection to pair by GRing.isMultiplicative.rmorphism_subproof in GRing_isMultiplicative__to__GRing_isMultiplicative: redundant with HB_unnamed_factory_827 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 53, characters 0-131: Warning: Ignoring canonical projection to pair by GRing.isMultiplicative.rmorphism_subproof in GRing_isMultiplicative__to__GRing_isMultiplicative: redundant with HB_unnamed_factory_827 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 60, characters 0-102: Warning: Ignoring canonical projection to pair by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_13: redundant with HB_unnamed_factory_824 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 67, characters 0-105: Warning: Ignoring canonical projection to pair by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_20: redundant with HB_unnamed_factory_827 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 72, characters 0-78: Warning: Ignoring canonical projection to eq_binP by hasDecEq.eqP in ssrnat.HB_unnamed_factory_3: redundant with ssrnat.HB_unnamed_factory_3 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 72, characters 0-78: Warning: Ignoring canonical projection to N.eqb by hasDecEq.eq_op in ssrnat.HB_unnamed_factory_3: redundant with ssrnat.HB_unnamed_factory_3 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 72, characters 0-78: Warning: Ignoring canonical projection to isCountable.pickleK by Choice_isCountable.pickleK in choice_Countable__to__choice_Choice_isCountable: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 72, characters 0-78: Warning: Ignoring canonical projection to isCountable.unpickle by Choice_isCountable.unpickle in choice_Countable__to__choice_Choice_isCountable: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 72, characters 0-78: Warning: Ignoring canonical projection to isCountable.pickle by Choice_isCountable.pickle in choice_Countable__to__choice_Choice_isCountable: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrC by GRing.SemiRing_hasCommutativeMul.mulrC in GRing_Nmodule_isComSemiRing__to__GRing_SemiRing_hasCommutativeMul: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_SemiRing_hasCommutativeMul [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.oner_neq0 by GRing.Nmodule_isSemiRing.oner_neq0 in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Builders_211.mulr0 by GRing.Nmodule_isSemiRing.mulr0 in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul0r by GRing.Nmodule_isSemiRing.mul0r in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Builders_211.mulrDr by GRing.Nmodule_isSemiRing.mulrDr in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrDl by GRing.Nmodule_isSemiRing.mulrDl in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Builders_211.mulr1 by GRing.Nmodule_isSemiRing.mulr1 in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul1r by GRing.Nmodule_isSemiRing.mul1r in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrA by GRing.Nmodule_isSemiRing.mulrA in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul by GRing.Nmodule_isSemiRing.mul in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 79, characters 0-142: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.one by GRing.Nmodule_isSemiRing.one in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 147, characters 0-76: Warning: Ignoring canonical projection to eqZP by hasDecEq.eqP in HB_unnamed_factory_45: redundant with HB_unnamed_factory_45 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 147, characters 0-76: Warning: Ignoring canonical projection to Z.eqb by hasDecEq.eq_op in HB_unnamed_factory_45: redundant with HB_unnamed_factory_45 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 147, characters 0-76: Warning: Ignoring canonical projection to isCountable.pickleK by Choice_isCountable.pickleK in choice_Countable__to__choice_Choice_isCountable__52: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 147, characters 0-76: Warning: Ignoring canonical projection to isCountable.unpickle by Choice_isCountable.unpickle in choice_Countable__to__choice_Choice_isCountable__52: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 147, characters 0-76: Warning: Ignoring canonical projection to isCountable.pickle by Choice_isCountable.pickle in choice_Countable__to__choice_Choice_isCountable__52: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 150, characters 0-109: Warning: Ignoring canonical projection to GRing.isZmodule.addNr by GRing.Nmodule_isZmodule.addNr in GRing_isZmodule__to__GRing_Nmodule_isZmodule: redundant with ssralg.GRing_isZmodule__to__GRing_Nmodule_isZmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 150, characters 0-109: Warning: Ignoring canonical projection to GRing.isZmodule.opp by GRing.Nmodule_isZmodule.opp in GRing_isZmodule__to__GRing_Nmodule_isZmodule: redundant with ssralg.GRing_isZmodule__to__GRing_Nmodule_isZmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 150, characters 0-109: Warning: Ignoring canonical projection to GRing.isZmodule.add0r by GRing.isNmodule.add0r in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 150, characters 0-109: Warning: Ignoring canonical projection to GRing.isZmodule.addrC by GRing.isNmodule.addrC in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 150, characters 0-109: Warning: Ignoring canonical projection to GRing.isZmodule.addrA by GRing.isNmodule.addrA in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 150, characters 0-109: Warning: Ignoring canonical projection to GRing.isZmodule.add by GRing.isNmodule.add in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 150, characters 0-109: Warning: Ignoring canonical projection to GRing.isZmodule.zero by GRing.isNmodule.zero in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Ring_hasCommutativeMul.mulrC by GRing.SemiRing_hasCommutativeMul.mulrC in GRing_Zmodule_isComRing__to__GRing_SemiRing_hasCommutativeMul: redundant with ssralg.GRing_Zmodule_isComRing__to__GRing_SemiRing_hasCommutativeMul [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.oner_neq0 by GRing.Nmodule_isSemiRing.oner_neq0 in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Builders_31.mulr0 by GRing.Nmodule_isSemiRing.mulr0 in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Builders_31.mul0r by GRing.Nmodule_isSemiRing.mul0r in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulrDr by GRing.Nmodule_isSemiRing.mulrDr in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulrDl by GRing.Nmodule_isSemiRing.mulrDl in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulr1 by GRing.Nmodule_isSemiRing.mulr1 in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mul1r by GRing.Nmodule_isSemiRing.mul1r in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulrA by GRing.Nmodule_isSemiRing.mulrA in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mul by GRing.Nmodule_isSemiRing.mul in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 154, characters 0-128: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.one by GRing.Nmodule_isSemiRing.one in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 170, characters 0-99: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.invr_out by GRing.Ring_hasMulInverse.invr_out_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 170, characters 0-99: Warning: Ignoring canonical projection to GRing.Builders_268.mulC_unitP by GRing.Ring_hasMulInverse.unitrP_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 170, characters 0-99: Warning: Ignoring canonical projection to GRing.Builders_268.mulC_mulrV by GRing.Ring_hasMulInverse.divrr_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 170, characters 0-99: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.mulVx by GRing.Ring_hasMulInverse.mulVr_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 170, characters 0-99: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.inv by GRing.Ring_hasMulInverse.inv in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 170, characters 0-99: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.unit by GRing.Ring_hasMulInverse.unit_subdef in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.meetP by Order.POrder_isMeetSemilattice.lexI in Num_IntegralDomain_isLeReal__to__Order_POrder_isMeetSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isMeetSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.meet by Order.POrder_isMeetSemilattice.meet in Num_IntegralDomain_isLeReal__to__Order_POrder_isMeetSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isMeetSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to order.Order.Builders_133.joinIl_subproof by Order.Lattice_isDistributive.joinIl in Num_IntegralDomain_isLeReal__to__Order_Lattice_isDistributive: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_Lattice_isDistributive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.Lattice_Meet_isDistrLattice.meetUl by Order.Lattice_isDistributive.meetUl in Num_IntegralDomain_isLeReal__to__Order_Lattice_isDistributive: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_Lattice_isDistributive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.Lattice_isTotal.le_total by Order.DistrLattice_isTotal.le_total in Num_IntegralDomain_isLeReal__to__Order_DistrLattice_isTotal: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_DistrLattice_isTotal [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.joinP by Order.POrder_isJoinSemilattice.leUx in Num_IntegralDomain_isLeReal__to__Order_POrder_isJoinSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isJoinSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.join by Order.POrder_isJoinSemilattice.join in Num_IntegralDomain_isLeReal__to__Order_POrder_isJoinSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isJoinSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.le_trans by Order.isDuallyPOrder.ge_trans in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.le_trans by Order.isDuallyPOrder.le_trans in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.Builders_90.ge_anti by Order.isDuallyPOrder.ge_anti in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.le_anti by Order.isDuallyPOrder.le_anti in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.le_refl by Order.isDuallyPOrder.ge_refl in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.le_refl by Order.isDuallyPOrder.le_refl in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.Builders_90.gt_def by Order.isDuallyPOrder.gt_def in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.lt_def by Order.isDuallyPOrder.lt_def in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.lt by Order.isDuallyPOrder.lt in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Order.isPOrder.le by Order.isDuallyPOrder.le in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.le_def by Num.isNumRing.ler_def in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.normM by Num.isNumRing.normrM in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.ger_total by Num.isNumRing.ger_leVge in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.addr_gt0 by Num.isNumRing.addr_gt0 in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.Builders_41.normrN by Num.Zmodule_isNormed.normrN in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.Builders_41.normrMn by Num.Zmodule_isNormed.normrMn in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.norm_eq0 by Num.Zmodule_isNormed.normr0_eq0 in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.normD by Num.Zmodule_isNormed.ler_normD in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 196, characters 0-149: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.norm by Num.Zmodule_isNormed.norm in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 211, characters 0-99: Warning: Ignoring canonical projection to pair_of_and by GRing.isSemiAdditive.semi_additive_subproof in GRing_isAdditive__to__GRing_isSemiAdditive: redundant with GRing.GRing_isAdditive__to__GRing_isSemiAdditive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 218, characters 0-99: Warning: Ignoring canonical projection to pair_of_and by GRing.isSemiAdditive.semi_additive_subproof in GRing_isAdditive__to__GRing_isSemiAdditive__90: redundant with GRing.GRing_isAdditive__to__GRing_isSemiAdditive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to add0n by GRing.isNmodule.add0r in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to addnC by GRing.isNmodule.addrC in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to addnA by GRing.isNmodule.addrA in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to addn by GRing.isNmodule.add in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to O by GRing.isNmodule.zero in HB_unnamed_factory_816: redundant with HB_unnamed_factory_816 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to nat by CountRing.Nmodule.sort in Datatypes_nat__canonical__CountRing_Nmodule: redundant with Datatypes_nat__canonical__CountRing_Nmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to nat by CountRing.SemiRing.sort in Datatypes_nat__canonical__CountRing_SemiRing: redundant with Datatypes_nat__canonical__CountRing_SemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to nat by CountRing.ComSemiRing.sort in Datatypes_nat__canonical__CountRing_ComSemiRing: redundant with Datatypes_nat__canonical__CountRing_ComSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrC by GRing.SemiRing_hasCommutativeMul.mulrC in HB_unnamed_mixin_822: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_SemiRing_hasCommutativeMul [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.oner_neq0 by GRing.Nmodule_isSemiRing.oner_neq0 in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_211.mulr0 by GRing.Nmodule_isSemiRing.mulr0 in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul0r by GRing.Nmodule_isSemiRing.mul0r in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_211.mulrDr by GRing.Nmodule_isSemiRing.mulrDr in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrDl by GRing.Nmodule_isSemiRing.mulrDl in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_211.mulr1 by GRing.Nmodule_isSemiRing.mulr1 in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul1r by GRing.Nmodule_isSemiRing.mul1r in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrA by GRing.Nmodule_isSemiRing.mulrA in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul by GRing.Nmodule_isSemiRing.mul in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.one by GRing.Nmodule_isSemiRing.one in HB_unnamed_mixin_821: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to pair by GRing.isSemiAdditive.semi_additive_subproof in GRing_isSemiAdditive__to__GRing_isSemiAdditive: redundant with HB_unnamed_factory_824 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to pair by GRing.isMultiplicative.rmorphism_subproof in GRing_isMultiplicative__to__GRing_isMultiplicative: redundant with HB_unnamed_factory_827 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to pair by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_13: redundant with HB_unnamed_factory_824 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to pair by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_20: redundant with HB_unnamed_factory_827 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to eq_binP by hasDecEq.eqP in ssrnat.HB_unnamed_factory_3: redundant with ssrnat.HB_unnamed_factory_3 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.eqb by hasDecEq.eq_op in ssrnat.HB_unnamed_factory_3: redundant with ssrnat.HB_unnamed_factory_3 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to isCountable.pickleK by Choice_isCountable.pickleK in choice_Countable__to__choice_Choice_isCountable: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to isCountable.unpickle by Choice_isCountable.unpickle in choice_Countable__to__choice_Choice_isCountable: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to isCountable.pickle by Choice_isCountable.pickle in choice_Countable__to__choice_Choice_isCountable: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by Choice.sort in BinNums_N__canonical__choice_Choice: redundant with BinNums_N__canonical__choice_Choice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by Countable.sort in BinNums_N__canonical__choice_Countable: redundant with BinNums_N__canonical__choice_Countable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.add_0_l by GRing.isNmodule.add0r in HB_unnamed_factory_22: redundant with HB_unnamed_factory_22 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.add_comm by GRing.isNmodule.addrC in HB_unnamed_factory_22: redundant with HB_unnamed_factory_22 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.add_assoc by GRing.isNmodule.addrA in HB_unnamed_factory_22: redundant with HB_unnamed_factory_22 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.add by GRing.isNmodule.add in HB_unnamed_factory_22: redundant with HB_unnamed_factory_22 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N0 by GRing.isNmodule.zero in HB_unnamed_factory_22: redundant with HB_unnamed_factory_22 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by GRing.Nmodule.sort in BinNums_N__canonical__GRing_Nmodule: redundant with BinNums_N__canonical__GRing_Nmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by CountRing.Nmodule.sort in BinNums_N__canonical__CountRing_Nmodule: redundant with BinNums_N__canonical__CountRing_Nmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrC by GRing.SemiRing_hasCommutativeMul.mulrC in GRing_Nmodule_isComSemiRing__to__GRing_SemiRing_hasCommutativeMul: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_SemiRing_hasCommutativeMul [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.oner_neq0 by GRing.Nmodule_isSemiRing.oner_neq0 in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_211.mulr0 by GRing.Nmodule_isSemiRing.mulr0 in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul0r by GRing.Nmodule_isSemiRing.mul0r in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_211.mulrDr by GRing.Nmodule_isSemiRing.mulrDr in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrDl by GRing.Nmodule_isSemiRing.mulrDl in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_211.mulr1 by GRing.Nmodule_isSemiRing.mulr1 in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul1r by GRing.Nmodule_isSemiRing.mul1r in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mulrA by GRing.Nmodule_isSemiRing.mulrA in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.mul by GRing.Nmodule_isSemiRing.mul in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Nmodule_isComSemiRing.one by GRing.Nmodule_isSemiRing.one in GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing: redundant with ssralg.GRing_Nmodule_isComSemiRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by GRing.SemiRing.sort in BinNums_N__canonical__GRing_SemiRing: redundant with BinNums_N__canonical__GRing_SemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by CountRing.SemiRing.sort in BinNums_N__canonical__CountRing_SemiRing: redundant with BinNums_N__canonical__CountRing_SemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by GRing.ComSemiRing.sort in BinNums_N__canonical__GRing_ComSemiRing: redundant with BinNums_N__canonical__GRing_ComSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N by CountRing.ComSemiRing.sort in BinNums_N__canonical__CountRing_ComSemiRing: redundant with BinNums_N__canonical__CountRing_ComSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to bin_of_nat_is_semi_additive by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_29: redundant with HB_unnamed_factory_29 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to bin_of_nat by GRing.Additive.sort in ssrnat_bin_of_nat__canonical__GRing_Additive: redundant with ssrnat_bin_of_nat__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to nat_of_bin_is_semi_additive by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_31: redundant with HB_unnamed_factory_31 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to nat_of_bin by GRing.Additive.sort in ssrnat_nat_of_bin__canonical__GRing_Additive: redundant with ssrnat_nat_of_bin__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to bin_of_nat_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_33: redundant with HB_unnamed_factory_33 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to bin_of_nat by GRing.RMorphism.sort in ssrnat_bin_of_nat__canonical__GRing_RMorphism: redundant with ssrnat_bin_of_nat__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to nat_of_bin_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_35: redundant with HB_unnamed_factory_35 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to nat_of_bin by GRing.RMorphism.sort in ssrnat_nat_of_bin__canonical__GRing_RMorphism: redundant with ssrnat_nat_of_bin__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N_of_nat_is_semi_additive by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_37: redundant with HB_unnamed_factory_37 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.of_nat by GRing.Additive.sort in N_of_nat__canonical__GRing_Additive: redundant with N_of_nat__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N_to_nat_is_semi_additive by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_39: redundant with HB_unnamed_factory_39 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.to_nat by GRing.Additive.sort in N_to_nat__canonical__GRing_Additive: redundant with N_to_nat__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N_of_nat_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_41: redundant with HB_unnamed_factory_41 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.of_nat by GRing.RMorphism.sort in N_of_nat__canonical__GRing_RMorphism: redundant with N_of_nat__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N_to_nat_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_43: redundant with HB_unnamed_factory_43 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to N.to_nat by GRing.RMorphism.sort in N_to_nat__canonical__GRing_RMorphism: redundant with N_to_nat__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to eqZP by hasDecEq.eqP in HB_unnamed_factory_45: redundant with HB_unnamed_factory_45 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z.eqb by hasDecEq.eq_op in HB_unnamed_factory_45: redundant with HB_unnamed_factory_45 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Equality.sort in BinNums_Z__canonical__eqtype_Equality: redundant with BinNums_Z__canonical__eqtype_Equality [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to isCountable.pickleK by Choice_isCountable.pickleK in choice_Countable__to__choice_Choice_isCountable__52: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to isCountable.unpickle by Choice_isCountable.unpickle in choice_Countable__to__choice_Choice_isCountable__52: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to isCountable.pickle by Choice_isCountable.pickle in choice_Countable__to__choice_Choice_isCountable__52: redundant with choice.choice_isCountable__to__choice_Choice_isCountable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Choice.sort in BinNums_Z__canonical__choice_Choice: redundant with BinNums_Z__canonical__choice_Choice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Countable.sort in BinNums_Z__canonical__choice_Countable: redundant with BinNums_Z__canonical__choice_Countable [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.isZmodule.addNr by GRing.Nmodule_isZmodule.addNr in GRing_isZmodule__to__GRing_Nmodule_isZmodule: redundant with ssralg.GRing_isZmodule__to__GRing_Nmodule_isZmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.isZmodule.opp by GRing.Nmodule_isZmodule.opp in GRing_isZmodule__to__GRing_Nmodule_isZmodule: redundant with ssralg.GRing_isZmodule__to__GRing_Nmodule_isZmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.isZmodule.add0r by GRing.isNmodule.add0r in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.isZmodule.addrC by GRing.isNmodule.addrC in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.isZmodule.addrA by GRing.isNmodule.addrA in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.isZmodule.add by GRing.isNmodule.add in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.isZmodule.zero by GRing.isNmodule.zero in GRing_isZmodule__to__GRing_isNmodule: redundant with ssralg.GRing_isZmodule__to__GRing_isNmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.Nmodule.sort in BinNums_Z__canonical__GRing_Nmodule: redundant with BinNums_Z__canonical__GRing_Nmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.Zmodule.sort in BinNums_Z__canonical__GRing_Zmodule: redundant with BinNums_Z__canonical__GRing_Zmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.Nmodule.sort in BinNums_Z__canonical__CountRing_Nmodule: redundant with BinNums_Z__canonical__CountRing_Nmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.Zmodule.sort in BinNums_Z__canonical__CountRing_Zmodule: redundant with BinNums_Z__canonical__CountRing_Zmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Ring_hasCommutativeMul.mulrC by GRing.SemiRing_hasCommutativeMul.mulrC in GRing_Zmodule_isComRing__to__GRing_SemiRing_hasCommutativeMul: redundant with ssralg.GRing_Zmodule_isComRing__to__GRing_SemiRing_hasCommutativeMul [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.oner_neq0 by GRing.Nmodule_isSemiRing.oner_neq0 in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_31.mulr0 by GRing.Nmodule_isSemiRing.mulr0 in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_31.mul0r by GRing.Nmodule_isSemiRing.mul0r in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulrDr by GRing.Nmodule_isSemiRing.mulrDr in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulrDl by GRing.Nmodule_isSemiRing.mulrDl in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulr1 by GRing.Nmodule_isSemiRing.mulr1 in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mul1r by GRing.Nmodule_isSemiRing.mul1r in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mulrA by GRing.Nmodule_isSemiRing.mulrA in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.mul by GRing.Nmodule_isSemiRing.mul in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Zmodule_isRing.one by GRing.Nmodule_isSemiRing.one in GRing_Zmodule_isComRing__to__GRing_Nmodule_isSemiRing: redundant with GRing_Zmodule_isRing__to__GRing_Nmodule_isSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.SemiRing.sort in BinNums_Z__canonical__GRing_SemiRing: redundant with BinNums_Z__canonical__GRing_SemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.SemiRing.sort in BinNums_Z__canonical__CountRing_SemiRing: redundant with BinNums_Z__canonical__CountRing_SemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.Ring.sort in BinNums_Z__canonical__GRing_Ring: redundant with BinNums_Z__canonical__GRing_Ring [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.Ring.sort in BinNums_Z__canonical__CountRing_Ring: redundant with BinNums_Z__canonical__CountRing_Ring [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.ComSemiRing.sort in BinNums_Z__canonical__GRing_ComSemiRing: redundant with BinNums_Z__canonical__GRing_ComSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.ComSemiRing.sort in BinNums_Z__canonical__CountRing_ComSemiRing: redundant with BinNums_Z__canonical__CountRing_ComSemiRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.ComRing.sort in BinNums_Z__canonical__GRing_ComRing: redundant with BinNums_Z__canonical__GRing_ComRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.ComRing.sort in BinNums_Z__canonical__CountRing_ComRing: redundant with BinNums_Z__canonical__CountRing_ComRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.invr_out by GRing.Ring_hasMulInverse.invr_out_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_268.mulC_unitP by GRing.Ring_hasMulInverse.unitrP_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.Builders_268.mulC_mulrV by GRing.Ring_hasMulInverse.divrr_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.mulVx by GRing.Ring_hasMulInverse.mulVr_subproof in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.inv by GRing.Ring_hasMulInverse.inv in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to GRing.ComRing_hasMulInverse.unit by GRing.Ring_hasMulInverse.unit_subdef in GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse: redundant with ssralg.GRing_ComRing_hasMulInverse__to__GRing_Ring_hasMulInverse [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.UnitRing.sort in BinNums_Z__canonical__GRing_UnitRing: redundant with BinNums_Z__canonical__GRing_UnitRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.UnitRing.sort in BinNums_Z__canonical__CountRing_UnitRing: redundant with BinNums_Z__canonical__CountRing_UnitRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.ComUnitRing.sort in BinNums_Z__canonical__GRing_ComUnitRing: redundant with BinNums_Z__canonical__GRing_ComUnitRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.ComUnitRing.sort in BinNums_Z__canonical__CountRing_ComUnitRing: redundant with BinNums_Z__canonical__CountRing_ComUnitRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to idomain_axiomZ by GRing.ComUnitRing_isIntegral.mulf_eq0_subproof in HB_unnamed_factory_68: redundant with HB_unnamed_factory_68 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by GRing.IntegralDomain.sort in BinNums_Z__canonical__GRing_IntegralDomain: redundant with BinNums_Z__canonical__GRing_IntegralDomain [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by CountRing.IntegralDomain.sort in BinNums_Z__canonical__CountRing_IntegralDomain: redundant with BinNums_Z__canonical__CountRing_IntegralDomain [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.meetP by Order.POrder_isMeetSemilattice.lexI in Num_IntegralDomain_isLeReal__to__Order_POrder_isMeetSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isMeetSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.meet by Order.POrder_isMeetSemilattice.meet in Num_IntegralDomain_isLeReal__to__Order_POrder_isMeetSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isMeetSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to order.Order.Builders_133.joinIl_subproof by Order.Lattice_isDistributive.joinIl in Num_IntegralDomain_isLeReal__to__Order_Lattice_isDistributive: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_Lattice_isDistributive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.Lattice_Meet_isDistrLattice.meetUl by Order.Lattice_isDistributive.meetUl in Num_IntegralDomain_isLeReal__to__Order_Lattice_isDistributive: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_Lattice_isDistributive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.Lattice_isTotal.le_total by Order.DistrLattice_isTotal.le_total in Num_IntegralDomain_isLeReal__to__Order_DistrLattice_isTotal: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_DistrLattice_isTotal [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.joinP by Order.POrder_isJoinSemilattice.leUx in Num_IntegralDomain_isLeReal__to__Order_POrder_isJoinSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isJoinSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.POrder_MeetJoin_isLattice.join by Order.POrder_isJoinSemilattice.join in Num_IntegralDomain_isLeReal__to__Order_POrder_isJoinSemilattice: redundant with @Order.DeprecatedSubOrder.Order_SubPOrder_isSubOrder__to__Order_POrder_isJoinSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.le_trans by Order.isDuallyPOrder.ge_trans in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.le_trans by Order.isDuallyPOrder.le_trans in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.Builders_90.ge_anti by Order.isDuallyPOrder.ge_anti in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.le_anti by Order.isDuallyPOrder.le_anti in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.le_refl by Order.isDuallyPOrder.ge_refl in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.le_refl by Order.isDuallyPOrder.le_refl in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.Builders_90.gt_def by Order.isDuallyPOrder.gt_def in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.lt_def by Order.isDuallyPOrder.lt_def in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.lt by Order.isDuallyPOrder.lt in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Order.isPOrder.le by Order.isDuallyPOrder.le in Num_IntegralDomain_isLeReal__to__Order_isDuallyPOrder: redundant with Order.NatOrder.Order_isOrder__to__Order_isDuallyPOrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.le_def by Num.isNumRing.ler_def in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.normM by Num.isNumRing.normrM in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.ger_total by Num.isNumRing.ger_leVge in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.addr_gt0 by Num.isNumRing.addr_gt0 in Num_IntegralDomain_isLeReal__to__Num_isNumRing: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_isNumRing [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.Builders_41.normrN by Num.Zmodule_isNormed.normrN in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.Builders_41.normrMn by Num.Zmodule_isNormed.normrMn in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.norm_eq0 by Num.Zmodule_isNormed.normr0_eq0 in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.normD by Num.Zmodule_isNormed.ler_normD in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Num.IntegralDomain_isNumRing.norm by Num.Zmodule_isNormed.norm in Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed: redundant with ssrint.Num_IntegralDomain_isLeReal__to__Num_Zmodule_isNormed [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Order.POrder.sort in BinNums_Z__canonical__Order_POrder: redundant with BinNums_Z__canonical__Order_POrder [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Num.POrderedZmodule.sort in BinNums_Z__canonical__Num_POrderedZmodule: redundant with BinNums_Z__canonical__Num_POrderedZmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Order.MeetSemilattice.sort in BinNums_Z__canonical__Order_MeetSemilattice: redundant with BinNums_Z__canonical__Order_MeetSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Order.JoinSemilattice.sort in BinNums_Z__canonical__Order_JoinSemilattice: redundant with BinNums_Z__canonical__Order_JoinSemilattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Order.Lattice.sort in BinNums_Z__canonical__Order_Lattice: redundant with BinNums_Z__canonical__Order_Lattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Order.DistrLattice.sort in BinNums_Z__canonical__Order_DistrLattice: redundant with BinNums_Z__canonical__Order_DistrLattice [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Order.Total.sort in BinNums_Z__canonical__Order_Total: redundant with BinNums_Z__canonical__Order_Total [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Num.NormedZmodule.sort in BinNums_Z__canonical__Num_NormedZmodule: redundant with BinNums_Z__canonical__Num_NormedZmodule [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Num.NumDomain.sort in BinNums_Z__canonical__Num_NumDomain: redundant with BinNums_Z__canonical__Num_NumDomain [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z by Num.RealDomain.sort in BinNums_Z__canonical__Num_RealDomain: redundant with BinNums_Z__canonical__Num_RealDomain [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to pair_of_and by GRing.isSemiAdditive.semi_additive_subproof in GRing_isAdditive__to__GRing_isSemiAdditive: redundant with GRing.GRing_isAdditive__to__GRing_isSemiAdditive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z_of_int by GRing.Additive.sort in ssrZ_Z_of_int__canonical__GRing_Additive: redundant with ssrZ_Z_of_int__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to pair_of_and by GRing.isSemiAdditive.semi_additive_subproof in GRing_isAdditive__to__GRing_isSemiAdditive__90: redundant with GRing.GRing_isAdditive__to__GRing_isSemiAdditive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to int_of_Z by GRing.Additive.sort in ssrZ_int_of_Z__canonical__GRing_Additive: redundant with ssrZ_int_of_Z__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z_of_int_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_92: redundant with HB_unnamed_factory_92 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z_of_int by GRing.RMorphism.sort in ssrZ_Z_of_int__canonical__GRing_RMorphism: redundant with ssrZ_Z_of_int__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to int_of_Z_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_94: redundant with HB_unnamed_factory_94 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to int_of_Z by GRing.RMorphism.sort in ssrZ_int_of_Z__canonical__GRing_RMorphism: redundant with ssrZ_int_of_Z__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z_of_nat_is_semi_additive by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_96: redundant with HB_unnamed_factory_96 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z.of_nat by GRing.Additive.sort in Z_of_nat__canonical__GRing_Additive: redundant with Z_of_nat__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z_of_nat_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_98: redundant with HB_unnamed_factory_98 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z.of_nat by GRing.RMorphism.sort in Z_of_nat__canonical__GRing_RMorphism: redundant with Z_of_nat__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z_of_N_is_semi_additive by GRing.isSemiAdditive.semi_additive_subproof in HB_unnamed_factory_100: redundant with HB_unnamed_factory_100 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z.of_N by GRing.Additive.sort in Z_of_N__canonical__GRing_Additive: redundant with Z_of_N__canonical__GRing_Additive [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z_of_N_is_multiplicative by GRing.isMultiplicative.rmorphism_subproof in HB_unnamed_factory_102: redundant with HB_unnamed_factory_102 [redundant-canonical-projection,records,default] File "./theories/ssrZ.v", line 264, characters 16-28: Warning: Ignoring canonical projection to Z.of_N by GRing.RMorphism.sort in Z_of_N__canonical__GRing_RMorphism: redundant with Z_of_N__canonical__GRing_RMorphism [redundant-canonical-projection,records,default] COQC theories/zify_algebra.v File "./theories/zify_algebra.v", line 6, characters 0-78: Warning: New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing [GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed. [ambiguous-paths,coercions,default] File "./theories/zify_algebra.v", line 6, characters 0-78: Warning: New coercion path [GRing.subring_closed_semi; GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing [GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed. New coercion path [GRing.subring_closed_semi; GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing [GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed. [ambiguous-paths,coercions,default] File "./theories/zify_algebra.v", line 6, characters 0-78: Warning: New coercion path [GRing.sdivr_closed_div; GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing [GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed. [ambiguous-paths,coercions,default] File "./theories/zify_algebra.v", line 6, characters 0-78: Warning: New coercion path [GRing.subalg_closedBM; GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing [GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed. [ambiguous-paths,coercions,default] File "./theories/zify_algebra.v", line 6, characters 0-78: Warning: New coercion path [GRing.divring_closed_div; GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing [GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed. [ambiguous-paths,coercions,default] File "./theories/zify_algebra.v", line 6, characters 0-78: Warning: New coercion path [GRing.divalg_closedBdiv; GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing [GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed. [ambiguous-paths,coercions,default] COQC theories/zify.v make[2]: Leaving directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' make[1]: Leaving directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' debian/rules override_dh_auto_test make[1]: Entering directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' # disabled, upstream doesn't maintain them make[1]: Leaving directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' create-stamp debian/debhelper-build-stamp dh_prep debian/rules override_dh_auto_install make[1]: Entering directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' make install DESTDIR=/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp make[2]: Entering directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' coq_makefile -f Make -o Makefile.coq make --no-print-directory -f Makefile.coq install INSTALL theories/ssrZ.vo /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify_ssreflect.vo /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify_algebra.vo /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify.vo /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/ssrZ.v /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify_ssreflect.v /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify_algebra.v /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify.v /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/ssrZ.glob /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify_ssreflect.glob /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify_algebra.glob /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ INSTALL theories/zify.glob /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/zify/ make[2]: Leaving directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' make[1]: Leaving directory '/build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16' dh_install dh_ocamldoc dh_installdocs dh_installchangelogs dh_perl dh_link dh_strip_nondeterminism dh_compress dh_fixperms dh_missing dh_dwz -a dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb dh_coq dh_ocaml dh_gencontrol dh_md5sums dh_builddeb dpkg-deb: building package 'libcoq-mathcomp-zify' in '../libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb'. dpkg-genbuildinfo -O../mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.buildinfo dpkg-genchanges -sa -O../mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.changes dpkg-genchanges: info: including full source code in upload dpkg-source --after-build . dpkg-buildpackage: info: full upload (original source is included) -------------------------------------------------------------------------------- Build finished at 2025-01-15T15:52:32Z Finished -------- I: Built successfully +------------------------------------------------------------------------------+ | Changes Wed, 15 Jan 2025 15:52:32 +0000 | +------------------------------------------------------------------------------+ mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.changes: ---------------------------------------------------- Format: 1.8 Date: Wed, 15 Jan 2025 16:51:26 +0100 Source: mathcomp-zify Binary: libcoq-mathcomp-zify Architecture: source amd64 Version: 1.5.0+2.0+8.16-4+ocaml1 Distribution: unstable Urgency: medium Maintainer: Debian OCaml Maintainers Changed-By: Anonymous Builder Description: libcoq-mathcomp-zify - Micromega arithmetic solvers for Mathematical Components Changes: mathcomp-zify (1.5.0+2.0+8.16-4+ocaml1) unstable-ocaml; urgency=medium . * Rebuild for transition ocaml-5.3.0 Checksums-Sha1: ed95107f1bd98fe217592d7fa9bb32d05891d61f 1273 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc cb3d53e9c1680fb90be08563bc6c0f14ce4779a2 21080 mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz e0fab1d1d6a0512e698200dce0876c3ff02d6479 8828 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz 56a25b7073d4f540e392228893aaef63fe5417b7 272508 libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb ddf7266fd09baaa7732188dee6c0c7bad2995127 7046 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.buildinfo Checksums-Sha256: 429264c00954254623e2122a31fc1c47109cc6163d89a09ce9377e2c7be177d3 1273 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc 5988389c6c8dfde4d2f3a370278c6b2aa1b5a0f56531cb30b0cce2d550b4387c 21080 mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz 398d7af1aa618f8c81a354ad05a1ac1d293b3e41fbeb6126a9850236ad009669 8828 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz 4c4632709dc63cdce66ae78cc1f6f9569d244b49fc20ee0bea63b16f108fd97a 272508 libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb 4e2ceba61363661d091c22dcfcbb9385530ff0b61b75a159ddea26974d2b7299 7046 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.buildinfo Files: b60c253edf1bc16e84ceb6db1597b3a6 1273 ocaml optional mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc c9d02b943ba8148a27ec3e02a21bdcf2 21080 ocaml optional mathcomp-zify_1.5.0+2.0+8.16.orig.tar.gz 2fa610a2a3a6325cb7de97fda1d14c9e 8828 ocaml optional mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.debian.tar.xz de0c4364685e3d8234b9f5bde294b57b 272508 ocaml optional libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb d76a1973ef573abccbd996607e6e82f2 7046 ocaml optional mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.buildinfo +------------------------------------------------------------------------------+ | Buildinfo Wed, 15 Jan 2025 15:52:32 +0000 | +------------------------------------------------------------------------------+ Format: 1.0 Source: mathcomp-zify Binary: libcoq-mathcomp-zify Architecture: amd64 source Version: 1.5.0+2.0+8.16-4+ocaml1 Checksums-Md5: b60c253edf1bc16e84ceb6db1597b3a6 1273 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc de0c4364685e3d8234b9f5bde294b57b 272508 libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb Checksums-Sha1: ed95107f1bd98fe217592d7fa9bb32d05891d61f 1273 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc 56a25b7073d4f540e392228893aaef63fe5417b7 272508 libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb Checksums-Sha256: 429264c00954254623e2122a31fc1c47109cc6163d89a09ce9377e2c7be177d3 1273 mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc 4c4632709dc63cdce66ae78cc1f6f9569d244b49fc20ee0bea63b16f108fd97a 272508 libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb Build-Origin: Debian Build-Architecture: amd64 Build-Date: Wed, 15 Jan 2025 15:52:32 +0000 Build-Path: /build/reproducible-path/mathcomp-zify-1.5.0+2.0+8.16 Installed-Build-Depends: autoconf (= 2.72-3), automake (= 1:1.16.5-1.3), autopoint (= 0.22.5-4), autotools-dev (= 20220109.1), base-files (= 13.6), base-passwd (= 3.6.6), bash (= 5.2.37-1), binutils (= 2.43.50.20250108-1), binutils-common (= 2.43.50.20250108-1), binutils-x86-64-linux-gnu (= 2.43.50.20250108-1), bsdextrautils (= 2.40.4-1), bsdutils (= 1:2.40.4-1), build-essential (= 12.12), bzip2 (= 1.0.8-6), coq (= 8.20.0+dfsg-1+ocaml1), coreutils (= 9.5-1+b1), cpp (= 4:14.2.0-1), cpp-14 (= 14.2.0-13), cpp-14-x86-64-linux-gnu (= 14.2.0-13), cpp-x86-64-linux-gnu (= 4:14.2.0-1), dash (= 0.5.12-11), debconf (= 1.5.89), debhelper (= 13.23), debianutils (= 5.21), dh-autoreconf (= 20), dh-coq (= 0.13+ocaml1), dh-ocaml (= 2.4+ocaml1), dh-strip-nondeterminism (= 1.14.0-1), diffutils (= 1:3.10-2), dpkg (= 1.22.13), dpkg-dev (= 1.22.13), dwz (= 0.15-1+b1), file (= 1:5.45-3+b1), findutils (= 4.10.0-3), g++ (= 4:14.2.0-1), g++-14 (= 14.2.0-13), g++-14-x86-64-linux-gnu (= 14.2.0-13), g++-x86-64-linux-gnu (= 4:14.2.0-1), gcc (= 4:14.2.0-1), gcc-14 (= 14.2.0-13), gcc-14-base (= 14.2.0-13), gcc-14-x86-64-linux-gnu (= 14.2.0-13), gcc-x86-64-linux-gnu (= 4:14.2.0-1), gettext (= 0.22.5-4), gettext-base (= 0.22.5-4), grep (= 3.11-4), groff-base (= 1.23.0-7), gzip (= 1.12-1.2), hostname (= 3.25), init-system-helpers (= 1.68), intltool-debian (= 0.35.0+20060710.6), libacl1 (= 2.3.2-2+b1), libarchive-zip-perl (= 1.68-1), libasan8 (= 14.2.0-13), libatomic1 (= 14.2.0-13), libattr1 (= 1:2.5.2-2), libaudit-common (= 1:4.0.2-2), libaudit1 (= 1:4.0.2-2), libbinutils (= 2.43.50.20250108-1), libblkid1 (= 2.40.4-1), libbz2-1.0 (= 1.0.8-6), libc-bin (= 2.40-5), libc-dev-bin (= 2.40-5), libc6 (= 2.40-5), libc6-dev (= 2.40-5), libcap-ng0 (= 0.8.5-4), libcap2 (= 1:2.66-5+b1), libcc1-0 (= 14.2.0-13), libcompiler-libs-ocaml-dev (= 5.3.0-1~exp2+ocaml1), libconfig-tiny-perl (= 2.30-1), libcoq-core-ocaml (= 8.20.0+dfsg-1+ocaml1), libcoq-core-ocaml-dev (= 8.20.0+dfsg-1+ocaml1), libcoq-elpi (= 2.3.0-1+ocaml1), libcoq-hierarchy-builder (= 1.8.0-1+ocaml1), libcoq-mathcomp-algebra (= 2.3.0-1+ocaml1), libcoq-mathcomp-fingroup (= 2.3.0-1+ocaml1), libcoq-mathcomp-ssreflect (= 2.3.0-1+ocaml1), libcoq-stdlib (= 8.20.0+dfsg-1+ocaml1), libcrypt-dev (= 1:4.4.36-5), libcrypt1 (= 1:4.4.36-5), libctf-nobfd0 (= 2.43.50.20250108-1), libctf0 (= 2.43.50.20250108-1), libdb5.3t64 (= 5.3.28+dfsg2-9), libdebconfclient0 (= 0.277), libdebhelper-perl (= 13.23), libdpkg-perl (= 1.22.13), libelf1t64 (= 0.192-4), libelpi-ocaml (= 2.0.5-1+ocaml1), libelpi-ocaml-dev (= 2.0.5-1+ocaml1), libexpat1 (= 2.6.4-1), libffi8 (= 3.4.6-1), libfile-stripnondeterminism-perl (= 1.14.0-1), libfindlib-ocaml (= 1.9.6-3+ocaml1), libfindlib-ocaml-dev (= 1.9.6-3+ocaml1), libgcc-14-dev (= 14.2.0-13), libgcc-s1 (= 14.2.0-13), libgdbm-compat4t64 (= 1.24-2), libgdbm6t64 (= 1.24-2), libgmp-dev (= 2:6.3.0+dfsg-3), libgmp10 (= 2:6.3.0+dfsg-3), libgmp3-dev (= 2:6.3.0+dfsg-3), libgmpxx4ldbl (= 2:6.3.0+dfsg-3), libgomp1 (= 14.2.0-13), libgprofng0 (= 2.43.50.20250108-1), libhwasan0 (= 14.2.0-13), libicu72 (= 72.1-6), libisl23 (= 0.27-1), libitm1 (= 14.2.0-13), libjansson4 (= 2.14-2+b3), liblsan0 (= 14.2.0-13), liblzma5 (= 5.6.3-1+b1), libmagic-mgc (= 1:5.45-3+b1), libmagic1t64 (= 1:5.45-3+b1), libmd0 (= 1.1.0-2+b1), libmenhir-ocaml-dev (= 20240715+ds-1+ocaml1), libmount1 (= 2.40.4-1), libmpc3 (= 1.3.1-1+b3), libmpfr6 (= 4.2.1-1+b2), libncurses-dev (= 6.5-2+b1), libncurses6 (= 6.5-2+b1), libncursesw6 (= 6.5-2+b1), libocaml-compiler-libs-ocaml-dev (= 0.17.0-1+ocaml1), libpam-modules (= 1.5.3-7+b1), libpam-modules-bin (= 1.5.3-7+b1), libpam-runtime (= 1.5.3-7), libpam0g (= 1.5.3-7+b1), libpcre2-8-0 (= 10.44-5), libperl5.40 (= 5.40.0-8), libpipeline1 (= 1.5.8-1), libppx-derivers-ocaml-dev (= 1.2.1-4+ocaml1), libppx-deriving-ocaml (= 6.0.3-1+ocaml1), libppx-deriving-ocaml-dev (= 6.0.3-1+ocaml1), libppxlib-ocaml-dev (= 0.34.0-1+ocaml1), libpython3-stdlib (= 3.13.1-2), libpython3.13-minimal (= 3.13.1-3), libpython3.13-stdlib (= 3.13.1-3), libquadmath0 (= 14.2.0-13), libre-ocaml-dev (= 1.12.0+really1.11.0-1+ocaml1), libreadline8t64 (= 8.2-6), libseccomp2 (= 2.5.5-2), libselinux1 (= 3.7-3+b1), libsexplib0-ocaml (= 0.17.0-1+ocaml1), libsexplib0-ocaml-dev (= 0.17.0-1+ocaml1), libsframe1 (= 2.43.50.20250108-1), libsmartcols1 (= 2.40.4-1), libsqlite3-0 (= 3.46.1-1), libssl3t64 (= 3.4.0-2), libstdc++-14-dev (= 14.2.0-13), libstdc++6 (= 14.2.0-13), libstdlib-ocaml (= 5.3.0-1~exp2+ocaml1), libstdlib-ocaml-dev (= 5.3.0-1~exp2+ocaml1), libsystemd0 (= 257.2-1), libtinfo6 (= 6.5-2+b1), libtool (= 2.5.4-2), libtsan2 (= 14.2.0-13), libubsan1 (= 14.2.0-13), libuchardet0 (= 0.0.8-1+b2), libudev1 (= 257.2-1), libunistring5 (= 1.3-1), libuuid1 (= 2.40.4-1), libxml2 (= 2.12.7+dfsg+really2.9.14-0.2+b1), libzarith-ocaml (= 1.14-1+ocaml1), libzarith-ocaml-dev (= 1.14-1+ocaml1), libzstd-dev (= 1.5.6+dfsg-2), libzstd1 (= 1.5.6+dfsg-2), linux-libc-dev (= 6.12.9-1), m4 (= 1.4.19-5), make (= 4.4.1-1), man-db (= 2.13.0-1), mawk (= 1.3.4.20240905-1), media-types (= 10.1.0), ncurses-base (= 6.5-2), ncurses-bin (= 6.5-2+b1), netbase (= 6.4), ocaml (= 5.3.0-1~exp2+ocaml1), ocaml-base (= 5.3.0-1~exp2+ocaml1), ocaml-findlib (= 1.9.6-3+ocaml1), ocaml-interp (= 5.3.0-1~exp2+ocaml1), openssl-provider-legacy (= 3.4.0-2), patch (= 2.7.6-7), perl (= 5.40.0-8), perl-base (= 5.40.0-8), perl-modules-5.40 (= 5.40.0-8), po-debconf (= 1.0.21+nmu1), python3 (= 3.13.1-2), python3-minimal (= 3.13.1-2), python3.13 (= 3.13.1-3), python3.13-minimal (= 3.13.1-3), readline-common (= 8.2-6), rpcsvc-proto (= 1.4.3-1), sed (= 4.9-2), sensible-utils (= 0.0.24), sysvinit-utils (= 3.13-1), tar (= 1.35+dfsg-3.1), tzdata (= 2024b-6), util-linux (= 2.40.4-1), xz-utils (= 5.6.3-1+b1), zlib1g (= 1:1.3.dfsg+really1.3.1-1+b1) Environment: DEB_BUILD_OPTIONS="parallel=1" LANG="C.UTF-8" LC_COLLATE="C.UTF-8" LC_CTYPE="C.UTF-8" MAKEFLAGS="" SOURCE_DATE_EPOCH="1736956286" +------------------------------------------------------------------------------+ | Package contents Wed, 15 Jan 2025 15:52:32 +0000 | +------------------------------------------------------------------------------+ libcoq-mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1_amd64.deb ------------------------------------------------------ new Debian package, version 2.0. size 272508 bytes: control archive=1184 bytes. 762 bytes, 20 lines control 1709 bytes, 16 lines md5sums Package: libcoq-mathcomp-zify Source: mathcomp-zify Version: 1.5.0+2.0+8.16-4+ocaml1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 976 Depends: libcoq-mathcomp-algebra-ji8b0 Suggests: ocaml-findlib Provides: libcoq-mathcomp-zify-ukq20 Section: ocaml Priority: optional Homepage: https://github.com/math-comp/mczify Description: Micromega arithmetic solvers for Mathematical Components This package enables the use of the micromega arithmetic solvers of Coq for goals stated with the Mathematical Components library, by extending the zify tactic. . 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 2025-01-15 15:51 ./ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/ -rw-r--r-- root/root 37256 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/ssrZ.glob -rw-r--r-- root/root 8219 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/ssrZ.v -rw-r--r-- root/root 268208 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/ssrZ.vo -rw-r--r-- root/root 332 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify.glob -rw-r--r-- root/root 163 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify.v -rw-r--r-- root/root 892 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify.vo -rw-r--r-- root/root 61923 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify_algebra.glob -rw-r--r-- root/root 18045 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify_algebra.v -rw-r--r-- root/root 266874 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify_algebra.vo -rw-r--r-- root/root 77489 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify_ssreflect.glob -rw-r--r-- root/root 21150 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify_ssreflect.v -rw-r--r-- root/root 187657 2025-01-15 15:51 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/zify/zify_ssreflect.vo drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/share/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/share/doc/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./usr/share/doc/libcoq-mathcomp-zify/ -rw-r--r-- root/root 1790 2023-07-11 13:37 ./usr/share/doc/libcoq-mathcomp-zify/README.md -rw-r--r-- root/root 680 2025-01-15 15:51 ./usr/share/doc/libcoq-mathcomp-zify/changelog.Debian.gz -rw-r--r-- root/root 22286 2024-12-05 16:01 ./usr/share/doc/libcoq-mathcomp-zify/copyright drwxr-xr-x root/root 0 2025-01-15 15:51 ./var/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./var/lib/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./var/lib/coq/ drwxr-xr-x root/root 0 2025-01-15 15:51 ./var/lib/coq/md5sums/ -rw-r--r-- root/root 5 2025-01-15 15:51 ./var/lib/coq/md5sums/libcoq-mathcomp-zify.checksum +------------------------------------------------------------------------------+ | Post Build Wed, 15 Jan 2025 15:52:33 +0000 | +------------------------------------------------------------------------------+ +------------------------------------------------------------------------------+ | Cleanup Wed, 15 Jan 2025 15:52:33 +0000 | +------------------------------------------------------------------------------+ Purging /build/reproducible-path Not cleaning session: cloned chroot in use +------------------------------------------------------------------------------+ | Summary Wed, 15 Jan 2025 15:52:34 +0000 | +------------------------------------------------------------------------------+ Build Architecture: amd64 Build Type: full Build-Space: 4360 Build-Time: 15 Distribution: unstable Host Architecture: amd64 Install-Time: 40 Job: /tmp/tmp.ben.transition-scripts.DShdWCKr3y/mathcomp-zify_1.5.0+2.0+8.16-4+ocaml1.dsc Machine Architecture: amd64 Package: mathcomp-zify Package-Time: 65 Source-Version: 1.5.0+2.0+8.16-4+ocaml1 Space: 4360 Status: successful Version: 1.5.0+2.0+8.16-4+ocaml1 -------------------------------------------------------------------------------- Finished at 2025-01-15T15:52:32Z Build needed 00:01:05, 4360k disk space