sbuild (Debian sbuild) 0.88.1 (16 December 2024) on derowd.up7.fr +==============================================================================+ | mathcomp-analysis 1.8.0-1+ocaml1 (amd64) Wed, 15 Jan 2025 15:52:47 +0000 | +==============================================================================+ Package: mathcomp-analysis Version: 1.8.0-1+ocaml1 Source Version: 1.8.0-1+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.nEqLkEbDbS... 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:52:52 +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 http://localhost:9999/debian unstable InRelease [205 kB] Get:5 file:/rebuilt ./ Packages [1299 kB] Get:6 http://localhost:9999/debian unstable/main amd64 Packages [9979 kB] Get:7 http://localhost:9999/debian unstable/contrib amd64 Packages [65.7 kB] Get:8 http://localhost:9999/debian unstable/non-free-firmware amd64 Packages [6912 B] Get:9 http://localhost:9999/debian unstable/non-free amd64 Packages [122 kB] Fetched 10.4 MB in 1s (14.3 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:52:54 +0000 | +------------------------------------------------------------------------------+ Local sources ------------- /tmp/tmp.ben.transition-scripts.aj4eFnelIL/mathcomp-analysis_1.8.0-1+ocaml1.dsc exists in /tmp/tmp.ben.transition-scripts.aj4eFnelIL; copying to chroot +------------------------------------------------------------------------------+ | Install package build dependencies Wed, 15 Jan 2025 15:52:55 +0000 | +------------------------------------------------------------------------------+ Setup apt archive ----------------- Merged Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libcoq-hierarchy-builder, libcoq-mathcomp-algebra, libcoq-mathcomp-field, libcoq-mathcomp-fingroup, libcoq-mathcomp-solvable, libcoq-mathcomp-ssreflect, libcoq-mathcomp-bigenough, libcoq-mathcomp-finmap, ocaml-dune, build-essential, fakeroot Filtered Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libcoq-hierarchy-builder, libcoq-mathcomp-algebra, libcoq-mathcomp-field, libcoq-mathcomp-fingroup, libcoq-mathcomp-solvable, libcoq-mathcomp-ssreflect, libcoq-mathcomp-bigenough, libcoq-mathcomp-finmap, ocaml-dune, build-essential, fakeroot dpkg-deb: warning: root directory /build/reproducible-path/resolver-XQcAwH/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-XQcAwH/apt_archive/sbuild-build-depends-main-dummy.deb'. Ign:1 copy:/build/reproducible-path/resolver-XQcAwH/apt_archive ./ InRelease Get:2 copy:/build/reproducible-path/resolver-XQcAwH/apt_archive ./ Release [609 B] Ign:3 copy:/build/reproducible-path/resolver-XQcAwH/apt_archive ./ Release.gpg Get:4 copy:/build/reproducible-path/resolver-XQcAwH/apt_archive ./ Sources [869 B] Get:5 copy:/build/reproducible-path/resolver-XQcAwH/apt_archive ./ Packages [901 B] Fetched 2379 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-bigenough libcoq-mathcomp-field libcoq-mathcomp-fingroup libcoq-mathcomp-finmap libcoq-mathcomp-solvable 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-dune 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-bigenough libcoq-mathcomp-field libcoq-mathcomp-fingroup libcoq-mathcomp-finmap libcoq-mathcomp-solvable 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-dune 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, 94 newly installed, 0 to remove and 0 not upgraded. Need to get 30.1 MB/404 MB of archives. After this operation, 1311 MB of additional disk space will be used. Get:1 file:/rebuilt ./ libcoq-stdlib 8.20.0+dfsg-1+ocaml1 [23.5 MB] Get:2 copy:/build/reproducible-path/resolver-XQcAwH/apt_archive ./ sbuild-build-depends-main-dummy 0.invalid.0 [972 B] 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 file:/rebuilt ./ libstdlib-ocaml 5.3.0-1~exp2+ocaml1 [604 kB] Get:7 file:/rebuilt ./ ocaml-base 5.3.0-1~exp2+ocaml1 [494 kB] Get:8 file:/rebuilt ./ libfindlib-ocaml 1.9.6-3+ocaml1 [180 kB] Get:9 http://localhost:9999/debian unstable/main amd64 python3-minimal amd64 3.13.1-2 [27.0 kB] Get:10 file:/rebuilt ./ libzarith-ocaml 1.14-1+ocaml1 [117 kB] Get:11 http://localhost:9999/debian unstable/main amd64 media-types all 10.1.0 [26.9 kB] Get:12 http://localhost:9999/debian unstable/main amd64 netbase all 6.4 [12.8 kB] Get:13 file:/rebuilt ./ libcoq-core-ocaml 8.20.0+dfsg-1+ocaml1 [26.0 MB] Get:14 http://localhost:9999/debian unstable/main amd64 tzdata all 2024b-6 [257 kB] Get:15 http://localhost:9999/debian unstable/main amd64 libffi8 amd64 3.4.6-1 [23.6 kB] Get:16 http://localhost:9999/debian unstable/main amd64 libncursesw6 amd64 6.5-2+b1 [136 kB] Get:17 http://localhost:9999/debian unstable/main amd64 readline-common all 8.2-6 [69.4 kB] Get:18 http://localhost:9999/debian unstable/main amd64 libreadline8t64 amd64 8.2-6 [169 kB] Get:19 http://localhost:9999/debian unstable/main amd64 libsqlite3-0 amd64 3.46.1-1 [913 kB] 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 file:/rebuilt ./ libstdlib-ocaml-dev 5.3.0-1~exp2+ocaml1 [7889 kB] Get:37 http://localhost:9999/debian unstable/main amd64 autotools-dev all 20220109.1 [51.6 kB] Get:38 http://localhost:9999/debian unstable/main amd64 automake all 1:1.16.5-1.3 [823 kB] Get:39 http://localhost:9999/debian unstable/main amd64 autopoint all 0.22.5-4 [723 kB] Get:40 http://localhost:9999/debian unstable/main amd64 libncurses6 amd64 6.5-2+b1 [105 kB] Get:41 http://localhost:9999/debian unstable/main amd64 libncurses-dev amd64 6.5-2+b1 [351 kB] Get:42 http://localhost:9999/debian unstable/main amd64 libzstd-dev amd64 1.5.6+dfsg-2 [365 kB] Get:43 http://localhost:9999/debian unstable/main amd64 libdebhelper-perl all 13.23 [90.6 kB] Get:44 http://localhost:9999/debian unstable/main amd64 libtool all 2.5.4-2 [539 kB] Get:45 http://localhost:9999/debian unstable/main amd64 dh-autoreconf all 20 [17.1 kB] Get:46 http://localhost:9999/debian unstable/main amd64 libarchive-zip-perl all 1.68-1 [104 kB] Get:47 http://localhost:9999/debian unstable/main amd64 libfile-stripnondeterminism-perl all 1.14.0-1 [19.5 kB] Get:48 http://localhost:9999/debian unstable/main amd64 dh-strip-nondeterminism all 1.14.0-1 [8448 B] Get:49 http://localhost:9999/debian unstable/main amd64 libelf1t64 amd64 0.192-4 [189 kB] Get:50 http://localhost:9999/debian unstable/main amd64 dwz amd64 0.15-1+b1 [110 kB] Get:51 http://localhost:9999/debian unstable/main amd64 libunistring5 amd64 1.3-1 [476 kB] Get:52 file:/rebuilt ./ libcompiler-libs-ocaml-dev 5.3.0-1~exp2+ocaml1 [48.2 MB] Get:53 http://localhost:9999/debian unstable/main amd64 libicu72 amd64 72.1-6 [9421 kB] Get:54 http://localhost:9999/debian unstable/main amd64 libxml2 amd64 2.12.7+dfsg+really2.9.14-0.2+b1 [699 kB] Get:55 http://localhost:9999/debian unstable/main amd64 gettext amd64 0.22.5-4 [1600 kB] Get:56 http://localhost:9999/debian unstable/main amd64 intltool-debian all 0.35.0+20060710.6 [22.9 kB] Get:57 http://localhost:9999/debian unstable/main amd64 po-debconf all 1.0.21+nmu1 [248 kB] Get:58 http://localhost:9999/debian unstable/main amd64 debhelper all 13.23 [919 kB] Get:59 http://localhost:9999/debian unstable/main amd64 libconfig-tiny-perl all 2.30-1 [18.9 kB] Get:60 http://localhost:9999/debian unstable/main amd64 libfakeroot amd64 1.36.2-1 [29.6 kB] Get:61 http://localhost:9999/debian unstable/main amd64 fakeroot amd64 1.36.2-1 [75.4 kB] Get:62 http://localhost:9999/debian unstable/main amd64 libgmpxx4ldbl amd64 2:6.3.0+dfsg-3 [329 kB] Get:63 http://localhost:9999/debian unstable/main amd64 libgmp-dev amd64 2:6.3.0+dfsg-3 [642 kB] Get:64 http://localhost:9999/debian unstable/main amd64 libgmp3-dev amd64 2:6.3.0+dfsg-3 [322 kB] 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] Get:90 file:/rebuilt ./ libcoq-mathcomp-bigenough 1.0.1-14+ocaml1 [21.7 kB] Get:91 file:/rebuilt ./ libcoq-mathcomp-solvable 2.3.0-1+ocaml1 [4881 kB] Get:92 file:/rebuilt ./ libcoq-mathcomp-field 2.3.0-1+ocaml1 [3452 kB] Get:93 file:/rebuilt ./ libcoq-mathcomp-finmap 2.1.0-3+ocaml1 [851 kB] Get:94 file:/rebuilt ./ ocaml-dune 3.17.1-2+ocaml1 [4836 kB] Preconfiguring packages ... Fetched 30.1 MB in 1s (30.2 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 libcoq-mathcomp-bigenough. Preparing to unpack .../73-libcoq-mathcomp-bigenough_1.0.1-14+ocaml1_amd64.deb ... Unpacking libcoq-mathcomp-bigenough (1.0.1-14+ocaml1) ... Selecting previously unselected package libcoq-mathcomp-solvable. Preparing to unpack .../74-libcoq-mathcomp-solvable_2.3.0-1+ocaml1_amd64.deb ... Unpacking libcoq-mathcomp-solvable (2.3.0-1+ocaml1) ... Selecting previously unselected package libcoq-mathcomp-field. Preparing to unpack .../75-libcoq-mathcomp-field_2.3.0-1+ocaml1_amd64.deb ... Unpacking libcoq-mathcomp-field (2.3.0-1+ocaml1) ... Selecting previously unselected package libcoq-mathcomp-finmap. Preparing to unpack .../76-libcoq-mathcomp-finmap_2.1.0-3+ocaml1_amd64.deb ... Unpacking libcoq-mathcomp-finmap (2.1.0-3+ocaml1) ... Selecting previously unselected package ocaml-dune. Preparing to unpack .../77-ocaml-dune_3.17.1-2+ocaml1_amd64.deb ... Unpacking ocaml-dune (3.17.1-2+ocaml1) ... Selecting previously unselected package sbuild-build-depends-main-dummy. Preparing to unpack .../78-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 ocaml-dune (3.17.1-2+ocaml1) ... Setting up tzdata (2024b-6) ... Current default time zone: 'Etc/UTC' Local time is now: Wed Jan 15 15:54:54 UTC 2025. Universal Time is now: Wed Jan 15 15:54:54 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-bigenough (1.0.1-14+ocaml1) ... Setting up libcoq-mathcomp-fingroup (2.3.0-1+ocaml1) ... Setting up libcoq-mathcomp-algebra (2.3.0-1+ocaml1) ... Setting up libcoq-mathcomp-finmap (2.1.0-3+ocaml1) ... Setting up libcoq-mathcomp-solvable (2.3.0-1+ocaml1) ... Setting up libcoq-mathcomp-field (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:55:13 +0000 | +------------------------------------------------------------------------------+ Arch check ok (amd64 included in any) +------------------------------------------------------------------------------+ | Build environment Wed, 15 Jan 2025 15:55:13 +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-bigenough_1.0.1-14+ocaml1 libcoq-mathcomp-field_2.3.0-1+ocaml1 libcoq-mathcomp-fingroup_2.3.0-1+ocaml1 libcoq-mathcomp-finmap_2.1.0-3+ocaml1 libcoq-mathcomp-solvable_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-dune_3.17.1-2+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:55:13 +0000 | +------------------------------------------------------------------------------+ Unpack source ------------- Format: 3.0 (quilt) Source: mathcomp-analysis Binary: libcoq-mathcomp-analysis, libcoq-mathcomp-classical Architecture: any Version: 1.8.0-1+ocaml1 Maintainer: Debian OCaml Maintainers Uploaders: Julien Puydt Homepage: https://github.com/math-comp/analysis Standards-Version: 4.7.0 Vcs-Browser: https://salsa.debian.org/ocaml-team/mathcomp-analysis Vcs-Git: https://salsa.debian.org/ocaml-team/mathcomp-analysis.git Testsuite: autopkgtest Testsuite-Triggers: coq Build-Depends: coq, debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-elpi, libcoq-hierarchy-builder, libcoq-mathcomp-algebra, libcoq-mathcomp-field, libcoq-mathcomp-fingroup, libcoq-mathcomp-solvable, libcoq-mathcomp-ssreflect, libcoq-mathcomp-bigenough, libcoq-mathcomp-finmap, ocaml-dune Package-List: libcoq-mathcomp-analysis deb ocaml optional arch=any libcoq-mathcomp-classical deb ocaml optional arch=any Checksums-Sha1: 345a25c9b82bd935288f9308ebbcd8dba487800a 860482 mathcomp-analysis_1.8.0.orig.tar.gz 066313a9fc168b39e5fe520ed26a78c3a41297af 9540 mathcomp-analysis_1.8.0-1+ocaml1.debian.tar.xz Checksums-Sha256: b963bce2a3fca42da7412fee8c2c78170f59c9c3a12dd77e00e52c987668708a 860482 mathcomp-analysis_1.8.0.orig.tar.gz 2c652afaf8e133fd2d2349a610a93774c1c06b4bdc0410eb7ad21aa18b6d8e55 9540 mathcomp-analysis_1.8.0-1+ocaml1.debian.tar.xz Files: 07eece2ee43d2e11de925e7661e7d677 860482 mathcomp-analysis_1.8.0.orig.tar.gz 34287fd05c8877bfd33b61b6bda20ef7 9540 mathcomp-analysis_1.8.0-1+ocaml1.debian.tar.xz dpkg-source: warning: extracting unsigned source package (mathcomp-analysis_1.8.0-1+ocaml1.dsc) dpkg-source: info: extracting mathcomp-analysis in /build/reproducible-path/mathcomp-analysis-1.8.0 dpkg-source: info: unpacking mathcomp-analysis_1.8.0.orig.tar.gz dpkg-source: info: unpacking mathcomp-analysis_1.8.0-1+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-analysis dpkg-buildpackage: info: source version 1.8.0-1+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-analysis-1.8.0' rm -f Makefile.coq Makefile.coq.conf Makefile.coq rm -f make[1]: Leaving directory '/build/reproducible-path/mathcomp-analysis-1.8.0' dh_ocamlclean dh_clean dpkg-source -b . dpkg-source: info: using source format '3.0 (quilt)' dpkg-source: info: building mathcomp-analysis using existing ./mathcomp-analysis_1.8.0.orig.tar.gz dpkg-source: info: building mathcomp-analysis in mathcomp-analysis_1.8.0-1+ocaml1.debian.tar.xz dpkg-source: info: building mathcomp-analysis in mathcomp-analysis_1.8.0-1+ocaml1.dsc debian/rules binary dh binary --with coq,ocaml dh_update_autotools_config dh_autoreconf dh_ocamlinit dh_auto_configure dh_auto_build make -j1 "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/mathcomp-analysis-1.8.0' /usr/bin/coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq make[2]: Entering directory '/build/reproducible-path/mathcomp-analysis-1.8.0' COQDEP VFILES COQC classical/mathcomp_extra.v File "./classical/mathcomp_extra.v", line 433, characters 13-28: Warning: Notation archiDomainType is deprecated since mathcomp 2.3.0. Use archiRealDomainType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] COQC classical/boolp.v File "./classical/boolp.v", line 487, characters 58-68: Warning: Notation idempotent is deprecated since mathcomp 2.3.0. use `idempotent_op` instead [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./classical/boolp.v", line 491, characters 54-64: Warning: Notation idempotent is deprecated since mathcomp 2.3.0. use `idempotent_op` instead [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] COQC classical/contra.v COQC classical/wochoice.v COQC classical/classical_sets.v File "./classical/classical_sets.v", line 671, characters 15-25: Warning: Notation idempotent is deprecated since mathcomp 2.3.0. use `idempotent_op` instead [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./classical/classical_sets.v", line 725, characters 15-25: Warning: Notation idempotent is deprecated since mathcomp 2.3.0. use `idempotent_op` instead [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./classical/classical_sets.v", line 3162, characters 2-35: Warning: Notation Order.hasRelativeComplement.Build is deprecated since mathcomp 2.3.0. Use BDistrLattice_hasSectionalComplement.Build instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./classical/classical_sets.v", line 3165, characters 28-53: Warning: Notation Order.hasComplement.Build is deprecated since mathcomp 2.3.0. Use CBDistrLattice_hasComplement.Build instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] COQC classical/functions.v File "./classical/functions.v", line 269, characters 2-57: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./classical/functions.v", line 303, characters 1-67: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./classical/functions.v", line 632, characters 0-69: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] COQC classical/cardinality.v COQC classical/fsbigop.v File "./classical/fsbigop.v", line 319, characters 25-37: Warning: Notation full_fsbigID is deprecated. Use fsbigID instead [deprecated-syntactic-definition,deprecated,default] File "./classical/fsbigop.v", line 319, characters 25-37: Warning: Notation full_fsbigID is deprecated. Use fsbigID instead [deprecated-syntactic-definition,deprecated,default] File "./classical/fsbigop.v", line 319, characters 25-37: Warning: Notation full_fsbigID is deprecated. Use fsbigID instead [deprecated-syntactic-definition,deprecated,default] COQC classical/set_interval.v COQC classical/classical_orders.v COQC classical/filter.v File "./classical/filter.v", line 172, characters 0-27: Warning: The default and global localities for this command outside sections are currently equivalent to the combination of the standard meaning of "global" (as described in the reference manual), "export" and re-exporting for every surrounding module. It will change to just "global" (with the meaning used by the "Set" command) in a future release. To preserve the current meaning in a forward compatible way, use the attribute "#[global,export]" and repeat the command with just "#[export]" in any surrounding modules. If you are fine with the change of semantics, disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] File "./classical/filter.v", line 235, characters 2-56: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] COQC classical/all_classical.v COQC reals/signed.v COQC reals/constructive_ereal.v File "./reals/constructive_ereal.v", line 2661, characters 34-45: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./reals/constructive_ereal.v", line 2661, characters 34-45: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] COQC reals/reals.v File "./reals/reals.v", line 118, characters 45-59: Warning: Notation Num.ArchiField is deprecated since mathcomp 2.3.0. Use Num.ArchiRealField instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./reals/reals.v", line 127, characters 4-18: Warning: Notation Num.ArchiField is deprecated since mathcomp 2.3.0. Use Num.ArchiRealField instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./reals/reals.v", line 667, characters 19-33: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./reals/reals.v", line 670, characters 26-40: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./reals/reals.v", line 678, characters 24-38: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] COQC reals/real_interval.v File "./reals/real_interval.v", line 278, characters 62-69: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 278, characters 62-69: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 278, characters 62-69: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 301, characters 29-36: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 301, characters 29-36: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 301, characters 29-36: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 301, characters 29-36: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 301, characters 29-36: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./reals/real_interval.v", line 301, characters 29-36: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] COQC reals/itv.v COQC reals/prodnormedzmodule.v COQC reals/nsatz_realtype.v COQC reals/all_reals.v COQC experimental_reals/xfinmap.v COQC experimental_reals/discrete.v COQC experimental_reals/realseq.v COQC experimental_reals/realsum.v COQC experimental_reals/distr.v COQC reals_stdlib/Rstruct.v File "./reals_stdlib/Rstruct.v", line 511, characters 29-36: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 512, characters 19-26: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 512, characters 19-26: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 512, characters 19-26: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 515, characters 30-37: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 516, characters 19-26: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 516, characters 19-26: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 516, characters 19-26: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 520, characters 27-34: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 522, characters 13-20: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 522, characters 13-20: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 522, characters 13-20: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 523, characters 39-46: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 523, characters 39-46: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 523, characters 39-46: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 525, characters 28-35: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 525, characters 28-35: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 525, characters 28-35: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 539, characters 2-9: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 539, characters 41-48: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 540, characters 33-40: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 540, characters 59-71: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 540, characters 33-40: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 540, characters 33-40: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 540, characters 59-71: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 540, characters 59-71: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 544, characters 37-44: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 546, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 546, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 546, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 549, characters 20-32: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 549, characters 20-32: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 549, characters 20-32: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 555, characters 2-9: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 555, characters 52-59: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 557, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 557, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 557, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 559, characters 28-40: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 559, characters 64-76: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 559, characters 28-40: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 559, characters 28-40: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 559, characters 64-76: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 559, characters 64-76: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 563, characters 51-58: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 565, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 565, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 565, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 567, characters 17-29: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 567, characters 17-29: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 567, characters 17-29: Warning: Reference bigrmax_dflt is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 575, characters 12-19: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 575, characters 55-62: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 578, characters 11-22: Warning: Reference bigmaxr_nil is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 578, characters 11-22: Warning: Reference bigmaxr_nil is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 578, characters 11-22: Warning: Reference bigmaxr_nil is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 579, characters 12-22: Warning: Reference bigmaxr_un is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 579, characters 12-22: Warning: Reference bigmaxr_un is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 579, characters 12-22: Warning: Reference bigmaxr_un is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 579, characters 12-22: Warning: Reference bigmaxr_un is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 579, characters 12-22: Warning: Reference bigmaxr_un is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 580, characters 11-23: Warning: Reference bigmaxr_cons is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 580, characters 29-41: Warning: Reference bigmaxr_cons is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 580, characters 11-23: Warning: Reference bigmaxr_cons is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 580, characters 11-23: Warning: Reference bigmaxr_cons is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 580, characters 29-41: Warning: Reference bigmaxr_cons is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 580, characters 29-41: Warning: Reference bigmaxr_cons is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 585, characters 29-36: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 587, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 587, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 587, characters 9-16: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 588, characters 8-19: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 588, characters 8-19: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 588, characters 8-19: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 595, characters 62-69: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 598, characters 38-49: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 598, characters 38-49: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 599, characters 20-31: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 599, characters 20-31: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 599, characters 20-31: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 605, characters 61-68: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 608, characters 37-48: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 608, characters 37-48: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 609, characters 20-31: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 609, characters 20-31: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 609, characters 20-31: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 614, characters 69-76: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 617, characters 11-23: Warning: Reference bigmaxr_lerP is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 617, characters 11-23: Warning: Reference bigmaxr_lerP is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 618, characters 19-30: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 618, characters 19-30: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 618, characters 19-30: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 635, characters 23-30: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 635, characters 58-65: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 637, characters 44-55: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 637, characters 44-55: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 637, characters 44-55: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 638, characters 30-43: Warning: Reference bigmaxr_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 638, characters 30-43: Warning: Reference bigmaxr_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 638, characters 30-43: Warning: Reference bigmaxr_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 640, characters 10-21: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 640, characters 10-21: Warning: Reference bigmaxr_mem is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 646, characters 2-9: Warning: Reference bigmaxr is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 650, characters 12-18: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 652, characters 8-19: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 652, characters 8-19: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 652, characters 8-19: Warning: Reference bigmaxr_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 653, characters 9-15: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 653, characters 9-15: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 653, characters 9-15: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 660, characters 10-16: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 662, characters 9-15: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 662, characters 9-15: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 662, characters 9-15: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 665, characters 10-23: Warning: Reference bigmaxr_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 665, characters 10-23: Warning: Reference bigmaxr_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 669, characters 41-53: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 677, characters 5-17: Warning: Reference index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 677, characters 23-29: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 679, characters 7-19: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 679, characters 7-19: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 679, characters 7-19: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 14-20: Warning: Reference ordnat is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 22-34: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 40-52: Warning: Reference index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 14-20: Warning: Reference ordnat is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 22-34: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 14-20: Warning: Reference ordnat is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 22-34: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 40-52: Warning: Reference index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 682, characters 40-52: Warning: Reference index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 683, characters 33-45: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 683, characters 33-45: Warning: Reference bmaxrf_index is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 689, characters 15-21: Warning: Reference bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 689, characters 38-50: Warning: Reference index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 691, characters 37-47: Warning: Reference bmaxrf_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 691, characters 64-79: Warning: Reference eq_index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 691, characters 37-47: Warning: Reference bmaxrf_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 691, characters 37-47: Warning: Reference bmaxrf_ler is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 691, characters 64-79: Warning: Reference eq_index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] File "./reals_stdlib/Rstruct.v", line 691, characters 64-79: Warning: Reference eq_index_bmaxrf is deprecated. To be removed. Use topology.v's bigmax/min lemmas instead. [deprecated-reference,deprecated,default] COQC theories/topology_theory/topology_structure.v COQC theories/topology_theory/uniform_structure.v COQC theories/topology_theory/pseudometric_structure.v File "./theories/topology_theory/pseudometric_structure.v", line 120, characters 0-105: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/topology_theory/pseudometric_structure.v", line 440, characters 0-63: Warning: non forgetful inheritance detected. You have two solutions: 1. (Best practice) Reorganize your hierarchy to make classical_sets_isPointed depend on GRing_Zmodule. See the paper "Competing inheritance paths in dependent type theory" (https://hal.inria.fr/hal-02463336) for more explanations 2. Use the attribute #[non_forgetful_inheritance] to disable this check. We strongly advise you encapsulate this instance inside a module, in order to isolate it from the rest of the code, and to be able to import it on demand. See the above paper and the file https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v to witness devastating effects. [HB.non-forgetful-inheritance,HB,elpi,default] COQC theories/topology_theory/compact.v COQC theories/topology_theory/product_topology.v File "./theories/topology_theory/product_topology.v", line 45, characters 0-65: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] COQC theories/topology_theory/order_topology.v COQC theories/topology_theory/bool_topology.v COQC theories/topology_theory/num_topology.v File "./theories/topology_theory/num_topology.v", line 71, characters 30-44: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] COQC theories/topology_theory/quotient_topology.v COQC theories/topology_theory/connected.v COQC theories/topology_theory/matrix_topology.v File "./theories/topology_theory/matrix_topology.v", line 59, characters 0-52: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/topology_theory/matrix_topology.v", line 154, characters 0-75: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/topology_theory/matrix_topology.v", line 155, characters 0-85: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/topology_theory/matrix_topology.v", line 157, characters 0-88: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/topology_theory/matrix_topology.v", line 159, characters 0-70: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/topology_theory/matrix_topology.v", line 161, characters 0-78: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] COQC theories/topology_theory/nat_topology.v File "./theories/topology_theory/nat_topology.v", line 45, characters 22-29: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/topology_theory/nat_topology.v", line 45, characters 22-29: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/topology_theory/nat_topology.v", line 45, characters 22-29: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] COQC theories/topology_theory/weak_topology.v COQC theories/topology_theory/subspace_topology.v File "./theories/topology_theory/subspace_topology.v", line 691, characters 0-99: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] COQC theories/topology_theory/subtype_topology.v COQC theories/topology_theory/supremum_topology.v COQC theories/topology_theory/one_point_compactification.v COQC theories/topology_theory/sigT_topology.v COQC theories/topology_theory/topology.v COQC theories/ereal.v COQC theories/separation_axioms.v COQC theories/function_spaces.v File "./theories/function_spaces.v", line 112, characters 0-27: Warning: The default and global localities for this command outside sections are currently equivalent to the combination of the standard meaning of "global" (as described in the reference manual), "export" and re-exporting for every surrounding module. It will change to just "global" (with the meaning used by the "Set" command) in a future release. To preserve the current meaning in a forward compatible way, use the attribute "#[global,export]" and repeat the command with just "#[export]" in any surrounding modules. If you are fine with the change of semantics, disable this warning. [deprecated-tacopt-without-locality,deprecated-since-8.17,deprecated,default] File "./theories/function_spaces.v", line 434, characters 0-120: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/function_spaces.v", line 517, characters 0-110: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/function_spaces.v", line 561, characters 0-173: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] COQC theories/tvs.v COQC theories/normedtype.v File "./theories/normedtype.v", line 278, characters 58-65: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/normedtype.v", line 278, characters 58-65: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/normedtype.v", line 278, characters 58-65: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/normedtype.v", line 281, characters 56-63: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/normedtype.v", line 281, characters 56-63: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/normedtype.v", line 281, characters 56-63: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/normedtype.v", line 491, characters 34-40: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 491, characters 34-40: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 493, characters 34-41: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 493, characters 34-41: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 495, characters 34-40: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 495, characters 34-40: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 497, characters 34-41: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 497, characters 34-41: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 939, characters 14-28: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/normedtype.v", line 956, characters 0-84: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/normedtype.v", line 980, characters 0-83: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/normedtype.v", line 3400, characters 24-38: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 3400, characters 24-38: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 3482, characters 24-42: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 3482, characters 24-42: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/normedtype.v", line 3935, characters 0-54: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/normedtype.v", line 4208, characters 0-63: Warning: non forgetful inheritance detected. You have two solutions: 1. (Best practice) Reorganize your hierarchy to make uniform_structure_Complete depend on reals_Real. See the paper "Competing inheritance paths in dependent type theory" (https://hal.inria.fr/hal-02463336) for more explanations 2. Use the attribute #[non_forgetful_inheritance] to disable this check. We strongly advise you encapsulate this instance inside a module, in order to isolate it from the rest of the code, and to be able to import it on demand. See the above paper and the file https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v to witness devastating effects. [HB.non-forgetful-inheritance,HB,elpi,default] File "./theories/normedtype.v", line 4246, characters 33-47: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/normedtype.v", line 4255, characters 38-52: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/normedtype.v", line 4267, characters 24-38: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] COQC theories/landau.v COQC theories/cantor.v COQC theories/forms.v COQC theories/derive.v COQC theories/sequences.v File "./theories/sequences.v", line 778, characters 24-38: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 786, characters 25-39: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 820, characters 13-27: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 854, characters 13-27: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 984, characters 26-40: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 993, characters 20-34: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 1016, characters 32-46: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 1024, characters 37-51: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 1044, characters 25-39: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 1048, characters 35-49: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 1407, characters 38-52: Warning: Notation archiFieldType is deprecated since mathcomp 2.3.0. Use archiRealFieldType instead. [deprecated-syntactic-definition-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-syntactic-definition,deprecated,default] File "./theories/sequences.v", line 2981, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/sequences.v", line 2981, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/sequences.v", line 2981, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/sequences.v", line 3084, characters 45-52: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/sequences.v", line 3084, characters 45-52: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/sequences.v", line 3084, characters 45-52: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] COQC theories/realfun.v File "./theories/realfun.v", line 190, characters 56-63: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/realfun.v", line 190, characters 56-63: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/realfun.v", line 190, characters 56-63: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/realfun.v", line 282, characters 51-62: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/realfun.v", line 282, characters 51-62: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/realfun.v", line 282, characters 51-62: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] COQC theories/convex.v COQC theories/exp.v COQC theories/trigo.v File "./theories/trigo.v", line 1105, characters 23-35: Warning: Reference mulr_sg_norm is deprecated since mathcomp 2.3.0. use `numEsg` instead [deprecated-reference-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-reference,deprecated,default] File "./theories/trigo.v", line 1105, characters 23-35: Warning: Reference mulr_sg_norm is deprecated since mathcomp 2.3.0. use `numEsg` instead [deprecated-reference-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-reference,deprecated,default] File "./theories/trigo.v", line 1105, characters 23-35: Warning: Reference mulr_sg_norm is deprecated since mathcomp 2.3.0. use `numEsg` instead [deprecated-reference-since-mathcomp-2.3.0,deprecated-since-mathcomp-2.3.0,deprecated-reference,deprecated,default] COQC theories/numfun.v File "./theories/numfun.v", line 275, characters 24-38: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/numfun.v", line 275, characters 24-38: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/numfun.v", line 277, characters 24-38: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/numfun.v", line 277, characters 24-38: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] COQC theories/esum.v COQC theories/measure.v File "./theories/measure.v", line 2010, characters 12-52: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/measure.v", line 2010, characters 12-52: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/measure.v", line 2010, characters 20-49: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/measure.v", line 2014, characters 4-33: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/measure.v", line 2139, characters 34-43: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/measure.v", line 2139, characters 34-43: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/measure.v", line 2275, characters 54-61: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/measure.v", line 2275, characters 54-61: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/measure.v", line 2275, characters 54-61: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/measure.v", line 5056, characters 0-54: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] COQC theories/lebesgue_stieltjes_measure.v COQC theories/lebesgue_measure.v File "./theories/lebesgue_measure.v", line 204, characters 0-41: Warning: non forgetful inheritance detected. You have two solutions: 1. (Best practice) Reorganize your hierarchy to make classical_sets_Pointed depend on reals_Real. See the paper "Competing inheritance paths in dependent type theory" (https://hal.inria.fr/hal-02463336) for more explanations 2. Use the attribute #[non_forgetful_inheritance] to disable this check. We strongly advise you encapsulate this instance inside a module, in order to isolate it from the rest of the code, and to be able to import it on demand. See the above paper and the file https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v to witness devastating effects. [HB.non-forgetful-inheritance,HB,elpi,default] File "./theories/lebesgue_measure.v", line 204, characters 0-41: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/lebesgue_measure.v", line 205, characters 0-197: Warning: non forgetful inheritance detected. You have two solutions: 1. (Best practice) Reorganize your hierarchy to make measure_isMeasurable depend on reals_Real. See the paper "Competing inheritance paths in dependent type theory" (https://hal.inria.fr/hal-02463336) for more explanations 2. Use the attribute #[non_forgetful_inheritance] to disable this check. We strongly advise you encapsulate this instance inside a module, in order to isolate it from the rest of the code, and to be able to import it on demand. See the above paper and the file https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v to witness devastating effects. [HB.non-forgetful-inheritance,HB,elpi,default] File "./theories/lebesgue_measure.v", line 456, characters 58-69: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 456, characters 58-69: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 456, characters 58-69: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 459, characters 50-61: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 459, characters 50-61: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 459, characters 50-61: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 3197, characters 48-55: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 3197, characters 48-55: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_measure.v", line 3197, characters 48-55: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] COQC theories/lebesgue_integral.v File "./theories/lebesgue_integral.v", line 314, characters 44-57: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/lebesgue_integral.v", line 496, characters 0-70: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/lebesgue_integral.v", line 684, characters 34-72: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/lebesgue_integral.v", line 684, characters 34-72: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/lebesgue_integral.v", line 684, characters 40-69: Warning: Cast types are ignored in patterns [cast-in-pattern,automation,default] File "./theories/lebesgue_integral.v", line 1740, characters 0-70: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/lebesgue_integral.v", line 1744, characters 0-88: Warning: HB: no new instance is generated [HB.no-new-instance,HB,elpi,default] File "./theories/lebesgue_integral.v", line 2353, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2353, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2353, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2353, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2353, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2353, characters 33-40: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2362, characters 28-39: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2362, characters 28-39: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2362, characters 28-39: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2383, characters 37-44: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2383, characters 37-44: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2383, characters 37-44: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2383, characters 37-44: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2383, characters 37-44: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2383, characters 37-44: Warning: Reference ceil_ge is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.le_ceil` instead [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2622, characters 23-34: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2622, characters 23-34: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2622, characters 23-34: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2632, characters 28-39: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2632, characters 28-39: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 2632, characters 28-39: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 3773, characters 24-35: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 3773, characters 24-35: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] File "./theories/lebesgue_integral.v", line 3773, characters 24-35: Warning: Reference ceil_ge_int is deprecated since mathcomp-analysis 1.3.0. use `Num.Theory.ceil_le_int` [deprecated-reference-since-mathcomp-analysis-1.3.0,deprecated-since-mathcomp-analysis-1.3.0,deprecated-reference,deprecated,default] COQC theories/charge.v COQC theories/ftc.v COQC theories/hoelder.v COQC theories/kernel.v COQC theories/probability.v COQC theories/all_analysis.v COQC theories/homotopy_theory/wedge_sigT.v COQC theories/homotopy_theory/continuous_path.v COQC theories/homotopy_theory/homotopy.v COQC theories/showcase/summability.v COQC analysis_stdlib/Rstruct_topology.v COQC analysis_stdlib/showcase/uniform_bigO.v make[2]: Leaving directory '/build/reproducible-path/mathcomp-analysis-1.8.0' make[1]: Leaving directory '/build/reproducible-path/mathcomp-analysis-1.8.0' dh_auto_test create-stamp debian/debhelper-build-stamp dh_prep dh_auto_install make -j1 install DESTDIR=/build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp AM_UPDATE_INFO_DIR=no "INSTALL=install --strip-program=true" make[1]: Entering directory '/build/reproducible-path/mathcomp-analysis-1.8.0' /usr/bin/coq_makefile -f _CoqProject -o Makefile.coq make -f Makefile.coq install make[2]: Entering directory '/build/reproducible-path/mathcomp-analysis-1.8.0' INSTALL classical/all_classical.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/boolp.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/contra.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/wochoice.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/classical_sets.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/mathcomp_extra.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/functions.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/cardinality.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/fsbigop.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/set_interval.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/classical_orders.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/filter.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL reals/constructive_ereal.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/reals.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/real_interval.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/signed.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/itv.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/prodnormedzmodule.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/nsatz_realtype.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/all_reals.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL experimental_reals/xfinmap.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/discrete.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/realseq.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/realsum.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/distr.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL reals_stdlib/Rstruct.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals_stdlib/ INSTALL theories/all_analysis.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/landau.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/topology_theory/topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/bool_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/compact.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/connected.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/matrix_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/nat_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/order_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/product_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/pseudometric_structure.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/subspace_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/subtype_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/supremum_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/topology_structure.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/uniform_structure.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/weak_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/num_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/quotient_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/one_point_compactification.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/sigT_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/homotopy_theory/homotopy.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/homotopy_theory/wedge_sigT.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/homotopy_theory/continuous_path.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/separation_axioms.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/function_spaces.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/ereal.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/cantor.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/tvs.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/normedtype.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/realfun.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/sequences.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/exp.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/trigo.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/esum.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_measure.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_stieltjes_measure.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/forms.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/derive.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/measure.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/numfun.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_integral.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/ftc.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/hoelder.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/probability.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/convex.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/charge.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/kernel.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/showcase/summability.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//showcase INSTALL analysis_stdlib/Rstruct_topology.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis_stdlib/ INSTALL analysis_stdlib/showcase/uniform_bigO.vo /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis_stdlib//showcase INSTALL classical/all_classical.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/boolp.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/contra.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/wochoice.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/classical_sets.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/mathcomp_extra.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/functions.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/cardinality.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/fsbigop.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/set_interval.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/classical_orders.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/filter.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL reals/constructive_ereal.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/reals.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/real_interval.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/signed.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/itv.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/prodnormedzmodule.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/nsatz_realtype.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/all_reals.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL experimental_reals/xfinmap.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/discrete.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/realseq.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/realsum.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/distr.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL reals_stdlib/Rstruct.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals_stdlib/ INSTALL theories/all_analysis.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/landau.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/topology_theory/topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/bool_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/compact.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/connected.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/matrix_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/nat_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/order_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/product_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/pseudometric_structure.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/subspace_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/subtype_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/supremum_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/topology_structure.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/uniform_structure.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/weak_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/num_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/quotient_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/one_point_compactification.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/sigT_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/homotopy_theory/homotopy.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/homotopy_theory/wedge_sigT.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/homotopy_theory/continuous_path.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/separation_axioms.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/function_spaces.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/ereal.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/cantor.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/tvs.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/normedtype.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/realfun.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/sequences.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/exp.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/trigo.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/esum.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_measure.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_stieltjes_measure.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/forms.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/derive.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/measure.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/numfun.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_integral.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/ftc.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/hoelder.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/probability.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/convex.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/charge.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/kernel.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/showcase/summability.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//showcase INSTALL analysis_stdlib/Rstruct_topology.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis_stdlib/ INSTALL analysis_stdlib/showcase/uniform_bigO.v /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis_stdlib//showcase INSTALL classical/all_classical.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/boolp.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/contra.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/wochoice.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/classical_sets.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/mathcomp_extra.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/functions.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/cardinality.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/fsbigop.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/set_interval.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/classical_orders.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL classical/filter.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/classical/ INSTALL reals/constructive_ereal.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/reals.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/real_interval.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/signed.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/itv.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/prodnormedzmodule.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/nsatz_realtype.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL reals/all_reals.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals/ INSTALL experimental_reals/xfinmap.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/discrete.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/realseq.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/realsum.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL experimental_reals/distr.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/experimental_reals/ INSTALL reals_stdlib/Rstruct.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/reals_stdlib/ INSTALL theories/all_analysis.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/landau.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/topology_theory/topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/bool_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/compact.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/connected.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/matrix_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/nat_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/order_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/product_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/pseudometric_structure.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/subspace_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/subtype_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/supremum_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/topology_structure.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/uniform_structure.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/weak_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/num_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/quotient_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/one_point_compactification.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/topology_theory/sigT_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//topology_theory INSTALL theories/homotopy_theory/homotopy.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/homotopy_theory/wedge_sigT.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/homotopy_theory/continuous_path.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//homotopy_theory INSTALL theories/separation_axioms.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/function_spaces.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/ereal.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/cantor.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/tvs.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/normedtype.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/realfun.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/sequences.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/exp.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/trigo.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/esum.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_measure.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_stieltjes_measure.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/forms.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/derive.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/measure.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/numfun.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/lebesgue_integral.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/ftc.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/hoelder.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/probability.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/convex.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/charge.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/kernel.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis/ INSTALL theories/showcase/summability.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis//showcase INSTALL analysis_stdlib/Rstruct_topology.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis_stdlib/ INSTALL analysis_stdlib/showcase/uniform_bigO.glob /build/reproducible-path/mathcomp-analysis-1.8.0/debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/mathcomp/analysis_stdlib//showcase make[3]: Entering directory '/build/reproducible-path/mathcomp-analysis-1.8.0' make[3]: Leaving directory '/build/reproducible-path/mathcomp-analysis-1.8.0' make[2]: Leaving directory '/build/reproducible-path/mathcomp-analysis-1.8.0' make[1]: Leaving directory '/build/reproducible-path/mathcomp-analysis-1.8.0' 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-analysis' in '../libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb'. dpkg-deb: building package 'libcoq-mathcomp-classical' in '../libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb'. dpkg-genbuildinfo -O../mathcomp-analysis_1.8.0-1+ocaml1_amd64.buildinfo dpkg-genchanges -sa -O../mathcomp-analysis_1.8.0-1+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-15T16:09:16Z Finished -------- I: Built successfully +------------------------------------------------------------------------------+ | Changes Wed, 15 Jan 2025 16:09:16 +0000 | +------------------------------------------------------------------------------+ mathcomp-analysis_1.8.0-1+ocaml1_amd64.changes: ----------------------------------------------- Format: 1.8 Date: Wed, 15 Jan 2025 16:52:46 +0100 Source: mathcomp-analysis Binary: libcoq-mathcomp-analysis libcoq-mathcomp-classical Architecture: source amd64 Version: 1.8.0-1+ocaml1 Distribution: unstable Urgency: medium Maintainer: Debian OCaml Maintainers Changed-By: Anonymous Builder Description: libcoq-mathcomp-analysis - analysis extension for Mathematical Components libcoq-mathcomp-classical - classical logic extension for Mathematical Components Changes: mathcomp-analysis (1.8.0-1+ocaml1) unstable-ocaml; urgency=medium . * Rebuild for transition ocaml-5.3.0 Checksums-Sha1: b64074504e86af105f6904a2dd09cd13494df52c 1545 mathcomp-analysis_1.8.0-1+ocaml1.dsc 345a25c9b82bd935288f9308ebbcd8dba487800a 860482 mathcomp-analysis_1.8.0.orig.tar.gz a76417ffc4014d6324c5c9912349a23d4ac4e60a 9544 mathcomp-analysis_1.8.0-1+ocaml1.debian.tar.xz f58fb01db0be9bbcb8fe1e367375178ad1c65544 16686752 libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb ab233415396bd5a45f04f055bebeabde772727f0 3436468 libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb 282a311114795231b5bc132351680e0e57db1443 7575 mathcomp-analysis_1.8.0-1+ocaml1_amd64.buildinfo Checksums-Sha256: f78444d7f7e83840ee7fe172567ca05ab3259181463ef9fadde119e72c7662f7 1545 mathcomp-analysis_1.8.0-1+ocaml1.dsc b963bce2a3fca42da7412fee8c2c78170f59c9c3a12dd77e00e52c987668708a 860482 mathcomp-analysis_1.8.0.orig.tar.gz d7f81700b9c874cf2f8e9ff44ecbf5795ba04575e0bae87fb645dce600112886 9544 mathcomp-analysis_1.8.0-1+ocaml1.debian.tar.xz dcaeb172bf5e880c7e29aadec003ba748d253d67113812d292d1343830e291ce 16686752 libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb 6e07be4f4da5017d3980309d80ab974d5fd1a7ea7073109895ee83dc854d2817 3436468 libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb cf1bacc536beebed24ec98bc4663e45c8d64077726f575879d7404441725c5be 7575 mathcomp-analysis_1.8.0-1+ocaml1_amd64.buildinfo Files: 6ed3e14806cdfc8218a31df18972882f 1545 ocaml optional mathcomp-analysis_1.8.0-1+ocaml1.dsc 07eece2ee43d2e11de925e7661e7d677 860482 ocaml optional mathcomp-analysis_1.8.0.orig.tar.gz 5af110dbedd7307350bae601ce41b9a0 9544 ocaml optional mathcomp-analysis_1.8.0-1+ocaml1.debian.tar.xz 3f34cfea1e102bed8f98082a9901cdd8 16686752 ocaml optional libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb de95f83282d40a558befa8c91cd7f4eb 3436468 ocaml optional libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb 38861eb9420857ba6500e24f39f3ed4a 7575 ocaml optional mathcomp-analysis_1.8.0-1+ocaml1_amd64.buildinfo +------------------------------------------------------------------------------+ | Buildinfo Wed, 15 Jan 2025 16:09:16 +0000 | +------------------------------------------------------------------------------+ Format: 1.0 Source: mathcomp-analysis Binary: libcoq-mathcomp-analysis libcoq-mathcomp-classical Architecture: amd64 source Version: 1.8.0-1+ocaml1 Checksums-Md5: 6ed3e14806cdfc8218a31df18972882f 1545 mathcomp-analysis_1.8.0-1+ocaml1.dsc 3f34cfea1e102bed8f98082a9901cdd8 16686752 libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb de95f83282d40a558befa8c91cd7f4eb 3436468 libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb Checksums-Sha1: b64074504e86af105f6904a2dd09cd13494df52c 1545 mathcomp-analysis_1.8.0-1+ocaml1.dsc f58fb01db0be9bbcb8fe1e367375178ad1c65544 16686752 libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb ab233415396bd5a45f04f055bebeabde772727f0 3436468 libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb Checksums-Sha256: f78444d7f7e83840ee7fe172567ca05ab3259181463ef9fadde119e72c7662f7 1545 mathcomp-analysis_1.8.0-1+ocaml1.dsc dcaeb172bf5e880c7e29aadec003ba748d253d67113812d292d1343830e291ce 16686752 libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb 6e07be4f4da5017d3980309d80ab974d5fd1a7ea7073109895ee83dc854d2817 3436468 libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb Build-Origin: Debian Build-Architecture: amd64 Build-Date: Wed, 15 Jan 2025 16:09:16 +0000 Build-Path: /build/reproducible-path/mathcomp-analysis-1.8.0 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-bigenough (= 1.0.1-14+ocaml1), libcoq-mathcomp-field (= 2.3.0-1+ocaml1), libcoq-mathcomp-fingroup (= 2.3.0-1+ocaml1), libcoq-mathcomp-finmap (= 2.1.0-3+ocaml1), libcoq-mathcomp-solvable (= 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-dune (= 3.17.1-2+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="1736956366" +------------------------------------------------------------------------------+ | Package contents Wed, 15 Jan 2025 16:09:16 +0000 | +------------------------------------------------------------------------------+ libcoq-mathcomp-analysis_1.8.0-1+ocaml1_amd64.deb ------------------------------------------------- new Debian package, version 2.0. size 16686752 bytes: control archive=5916 bytes. 958 bytes, 18 lines control 25494 bytes, 202 lines md5sums Package: libcoq-mathcomp-analysis Source: mathcomp-analysis Version: 1.8.0-1+ocaml1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 65968 Depends: libcoq-elpi-mm7d5, libcoq-hierarchy-builder-jjtu2, libcoq-mathcomp-algebra-ji8b0, libcoq-mathcomp-field-8igc5, libcoq-mathcomp-fingroup-hx5h8, libcoq-mathcomp-solvable-hxm24, libcoq-mathcomp-ssreflect-zgl00, libcoq-mathcomp-bigenough-vaxt3, libcoq-mathcomp-finmap-g98h5, libcoq-mathcomp-classical (= 1.8.0-1+ocaml1) Provides: libcoq-mathcomp-analysis-kq4m1 Section: ocaml Priority: optional Homepage: https://github.com/math-comp/analysis Description: analysis extension for Mathematical Components This package provides an extension for classical analysis for the Mathematical Components library. . 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:52 ./ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/ -rw-r--r-- root/root 1248 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/all_analysis.glob -rw-r--r-- root/root 992 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/all_analysis.v -rw-r--r-- root/root 2321 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/all_analysis.vo -rw-r--r-- root/root 126422 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/cantor.glob -rw-r--r-- root/root 23570 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/cantor.v -rw-r--r-- root/root 407562 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/cantor.vo -rw-r--r-- root/root 694864 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/charge.glob -rw-r--r-- root/root 86697 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/charge.v -rw-r--r-- root/root 1177718 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/charge.vo -rw-r--r-- root/root 114026 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/convex.glob -rw-r--r-- root/root 11376 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/convex.v -rw-r--r-- root/root 280527 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/convex.vo -rw-r--r-- root/root 688010 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/derive.glob -rw-r--r-- root/root 66868 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/derive.v -rw-r--r-- root/root 857278 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/derive.vo -rw-r--r-- root/root 469016 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/ereal.glob -rw-r--r-- root/root 58612 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/ereal.v -rw-r--r-- root/root 595244 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/ereal.vo -rw-r--r-- root/root 276173 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/esum.glob -rw-r--r-- root/root 28326 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/esum.v -rw-r--r-- root/root 333617 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/esum.vo -rw-r--r-- root/root 483095 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/exp.glob -rw-r--r-- root/root 43086 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/exp.v -rw-r--r-- root/root 489451 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/exp.vo -rw-r--r-- root/root 141731 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/forms.glob -rw-r--r-- root/root 20975 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/forms.v -rw-r--r-- root/root 380216 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/forms.vo -rw-r--r-- root/root 381327 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/ftc.glob -rw-r--r-- root/root 45053 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/ftc.v -rw-r--r-- root/root 462214 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/ftc.vo -rw-r--r-- root/root 443461 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/function_spaces.glob -rw-r--r-- root/root 68195 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/function_spaces.v -rw-r--r-- root/root 1179405 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/function_spaces.vo -rw-r--r-- root/root 260844 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/hoelder.glob -rw-r--r-- root/root 22880 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/hoelder.v -rw-r--r-- root/root 244820 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/hoelder.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/ -rw-r--r-- root/root 44811 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/continuous_path.glob -rw-r--r-- root/root 7062 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/continuous_path.v -rw-r--r-- root/root 266036 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/continuous_path.vo -rw-r--r-- root/root 217 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/homotopy.glob -rw-r--r-- root/root 168 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/homotopy.v -rw-r--r-- root/root 861 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/homotopy.vo -rw-r--r-- root/root 107410 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/wedge_sigT.glob -rw-r--r-- root/root 18200 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/wedge_sigT.v -rw-r--r-- root/root 315930 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/homotopy_theory/wedge_sigT.vo -rw-r--r-- root/root 381855 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/kernel.glob -rw-r--r-- root/root 43615 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/kernel.v -rw-r--r-- root/root 1033335 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/kernel.vo -rw-r--r-- root/root 405950 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/landau.glob -rw-r--r-- root/root 65058 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/landau.v -rw-r--r-- root/root 614586 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/landau.vo -rw-r--r-- root/root 3100228 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_integral.glob -rw-r--r-- root/root 305262 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_integral.v -rw-r--r-- root/root 3489167 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_integral.vo -rw-r--r-- root/root 1176880 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_measure.glob -rw-r--r-- root/root 142443 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_measure.v -rw-r--r-- root/root 1512966 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_measure.vo -rw-r--r-- root/root 201543 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_stieltjes_measure.glob -rw-r--r-- root/root 23418 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_stieltjes_measure.v -rw-r--r-- root/root 492784 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/lebesgue_stieltjes_measure.vo -rw-r--r-- root/root 1537272 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/measure.glob -rw-r--r-- root/root 217118 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/measure.v -rw-r--r-- root/root 3742015 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/measure.vo -rw-r--r-- root/root 2371926 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/normedtype.glob -rw-r--r-- root/root 254776 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/normedtype.v -rw-r--r-- root/root 4716880 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/normedtype.vo -rw-r--r-- root/root 232267 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/numfun.glob -rw-r--r-- root/root 25954 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/numfun.v -rw-r--r-- root/root 502733 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/numfun.vo -rw-r--r-- root/root 604869 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/probability.glob -rw-r--r-- root/root 56392 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/probability.v -rw-r--r-- root/root 766123 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/probability.vo -rw-r--r-- root/root 929543 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/realfun.glob -rw-r--r-- root/root 112071 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/realfun.v -rw-r--r-- root/root 1451650 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/realfun.vo -rw-r--r-- root/root 271427 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/separation_axioms.glob -rw-r--r-- root/root 45707 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/separation_axioms.v -rw-r--r-- root/root 605800 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/separation_axioms.vo -rw-r--r-- root/root 1064607 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/sequences.glob -rw-r--r-- root/root 133921 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/sequences.v -rw-r--r-- root/root 1151091 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/sequences.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/showcase/ -rw-r--r-- root/root 7503 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/showcase/summability.glob -rw-r--r-- root/root 1924 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/showcase/summability.v -rw-r--r-- root/root 39435 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/showcase/summability.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/ -rw-r--r-- root/root 7330 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/bool_topology.glob -rw-r--r-- root/root 2168 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/bool_topology.v -rw-r--r-- root/root 123585 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/bool_topology.vo -rw-r--r-- root/root 110606 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/compact.glob -rw-r--r-- root/root 20407 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/compact.v -rw-r--r-- root/root 182908 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/compact.vo -rw-r--r-- root/root 62012 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/connected.glob -rw-r--r-- root/root 9898 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/connected.v -rw-r--r-- root/root 95179 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/connected.vo -rw-r--r-- root/root 95543 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/matrix_topology.glob -rw-r--r-- root/root 9300 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/matrix_topology.v -rw-r--r-- root/root 266039 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/matrix_topology.vo -rw-r--r-- root/root 36351 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/nat_topology.glob -rw-r--r-- root/root 5463 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/nat_topology.v -rw-r--r-- root/root 163136 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/nat_topology.vo -rw-r--r-- root/root 60443 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/num_topology.glob -rw-r--r-- root/root 6603 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/num_topology.v -rw-r--r-- root/root 497831 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/num_topology.vo -rw-r--r-- root/root 21390 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/one_point_compactification.glob -rw-r--r-- root/root 4599 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/one_point_compactification.v -rw-r--r-- root/root 170165 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/one_point_compactification.vo -rw-r--r-- root/root 108520 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/order_topology.glob -rw-r--r-- root/root 12543 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/order_topology.v -rw-r--r-- root/root 610303 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/order_topology.vo -rw-r--r-- root/root 86181 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/product_topology.glob -rw-r--r-- root/root 10132 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/product_topology.v -rw-r--r-- root/root 232502 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/product_topology.vo -rw-r--r-- root/root 170452 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/pseudometric_structure.glob -rw-r--r-- root/root 22044 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/pseudometric_structure.v -rw-r--r-- root/root 675212 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/pseudometric_structure.vo -rw-r--r-- root/root 15365 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/quotient_topology.glob -rw-r--r-- root/root 2954 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/quotient_topology.v -rw-r--r-- root/root 160988 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/quotient_topology.vo -rw-r--r-- root/root 19816 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/sigT_topology.glob -rw-r--r-- root/root 3506 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/sigT_topology.v -rw-r--r-- root/root 139554 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/sigT_topology.vo -rw-r--r-- root/root 203689 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/subspace_topology.glob -rw-r--r-- root/root 27721 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/subspace_topology.v -rw-r--r-- root/root 419394 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/subspace_topology.vo -rw-r--r-- root/root 28413 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/subtype_topology.glob -rw-r--r-- root/root 6342 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/subtype_topology.v -rw-r--r-- root/root 193834 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/subtype_topology.vo -rw-r--r-- root/root 69133 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/supremum_topology.glob -rw-r--r-- root/root 9877 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/supremum_topology.v -rw-r--r-- root/root 232470 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/supremum_topology.vo -rw-r--r-- root/root 1330 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/topology.glob -rw-r--r-- root/root 913 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/topology.v -rw-r--r-- root/root 2843 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/topology.vo -rw-r--r-- root/root 297689 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/topology_structure.glob -rw-r--r-- root/root 39753 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/topology_structure.v -rw-r--r-- root/root 725797 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/topology_structure.vo -rw-r--r-- root/root 94913 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/uniform_structure.glob -rw-r--r-- root/root 14276 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/uniform_structure.v -rw-r--r-- root/root 501126 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/uniform_structure.vo -rw-r--r-- root/root 54384 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/weak_topology.glob -rw-r--r-- root/root 8729 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/weak_topology.v -rw-r--r-- root/root 240180 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/topology_theory/weak_topology.vo -rw-r--r-- root/root 512173 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/trigo.glob -rw-r--r-- root/root 47419 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/trigo.v -rw-r--r-- root/root 485151 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/trigo.vo -rw-r--r-- root/root 194951 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/tvs.glob -rw-r--r-- root/root 18931 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/tvs.v -rw-r--r-- root/root 878144 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis/tvs.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/ -rw-r--r-- root/root 16675 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/Rstruct_topology.glob -rw-r--r-- root/root 3381 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/Rstruct_topology.v -rw-r--r-- root/root 165130 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/Rstruct_topology.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/showcase/ -rw-r--r-- root/root 40785 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/showcase/uniform_bigO.glob -rw-r--r-- root/root 4617 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/showcase/uniform_bigO.v -rw-r--r-- root/root 93181 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/analysis_stdlib/showcase/uniform_bigO.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/ -rw-r--r-- root/root 34662 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/discrete.glob -rw-r--r-- root/root 6337 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/discrete.v -rw-r--r-- root/root 167250 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/discrete.vo -rw-r--r-- root/root 411137 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/distr.glob -rw-r--r-- root/root 44190 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/distr.v -rw-r--r-- root/root 410205 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/distr.vo -rw-r--r-- root/root 150916 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/realseq.glob -rw-r--r-- root/root 19679 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/realseq.v -rw-r--r-- root/root 210954 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/realseq.vo -rw-r--r-- root/root 423875 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/realsum.glob -rw-r--r-- root/root 46101 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/realsum.v -rw-r--r-- root/root 383012 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/realsum.vo -rw-r--r-- root/root 48078 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/xfinmap.glob -rw-r--r-- root/root 5608 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/xfinmap.v -rw-r--r-- root/root 66370 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/experimental_reals/xfinmap.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/ -rw-r--r-- root/root 383 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/all_reals.glob -rw-r--r-- root/root 293 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/all_reals.v -rw-r--r-- root/root 1326 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/all_reals.vo -rw-r--r-- root/root 2319065 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/constructive_ereal.glob -rw-r--r-- root/root 151642 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/constructive_ereal.v -rw-r--r-- root/root 2408156 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/constructive_ereal.vo -rw-r--r-- root/root 210540 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/itv.glob -rw-r--r-- root/root 35881 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/itv.v -rw-r--r-- root/root 414315 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/itv.vo -rw-r--r-- root/root 6623 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/nsatz_realtype.glob -rw-r--r-- root/root 2760 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/nsatz_realtype.v -rw-r--r-- root/root 57134 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/nsatz_realtype.vo -rw-r--r-- root/root 18708 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/prodnormedzmodule.glob -rw-r--r-- root/root 2425 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/prodnormedzmodule.v -rw-r--r-- root/root 132942 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/prodnormedzmodule.vo -rw-r--r-- root/root 155755 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/real_interval.glob -rw-r--r-- root/root 12186 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/real_interval.v -rw-r--r-- root/root 198540 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/real_interval.vo -rw-r--r-- root/root 189185 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/reals.glob -rw-r--r-- root/root 26473 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/reals.v -rw-r--r-- root/root 567371 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/reals.vo -rw-r--r-- root/root 839899 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/signed.glob -rw-r--r-- root/root 52158 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/signed.v -rw-r--r-- root/root 1134893 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals/signed.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals_stdlib/ -rw-r--r-- root/root 153422 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals_stdlib/Rstruct.glob -rw-r--r-- root/root 24995 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals_stdlib/Rstruct.v -rw-r--r-- root/root 361003 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/reals_stdlib/Rstruct.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/share/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/share/doc/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/share/doc/libcoq-mathcomp-analysis/ -rw-r--r-- root/root 155 2024-12-18 23:35 ./usr/share/doc/libcoq-mathcomp-analysis/CHANGELOG_UNRELEASED.md -rw-r--r-- root/root 1987 2024-12-18 23:35 ./usr/share/doc/libcoq-mathcomp-analysis/CONTRIBUTING.md.gz -rw-r--r-- root/root 3117 2024-12-18 23:35 ./usr/share/doc/libcoq-mathcomp-analysis/README.md.gz -rw-r--r-- root/root 1306 2025-01-15 15:52 ./usr/share/doc/libcoq-mathcomp-analysis/changelog.Debian.gz -rw-r--r-- root/root 67337 2024-12-18 23:35 ./usr/share/doc/libcoq-mathcomp-analysis/changelog.gz -rw-r--r-- root/root 22511 2024-12-26 09:07 ./usr/share/doc/libcoq-mathcomp-analysis/copyright drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/lib/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/lib/coq/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/lib/coq/md5sums/ -rw-r--r-- root/root 5 2025-01-15 15:52 ./var/lib/coq/md5sums/libcoq-mathcomp-analysis.checksum libcoq-mathcomp-classical_1.8.0-1+ocaml1_amd64.deb -------------------------------------------------- new Debian package, version 2.0. size 3436468 bytes: control archive=1876 bytes. 1052 bytes, 21 lines control 4725 bytes, 40 lines md5sums Package: libcoq-mathcomp-classical Source: mathcomp-analysis Version: 1.8.0-1+ocaml1 Architecture: amd64 Maintainer: Debian OCaml Maintainers Installed-Size: 13108 Depends: libcoq-elpi-mm7d5, libcoq-hierarchy-builder-jjtu2, libcoq-mathcomp-algebra-ji8b0, libcoq-mathcomp-field-8igc5, libcoq-mathcomp-fingroup-hx5h8, libcoq-mathcomp-solvable-hxm24, libcoq-mathcomp-ssreflect-zgl00, libcoq-mathcomp-bigenough-vaxt3, libcoq-mathcomp-finmap-g98h5 Breaks: libcoq-mathcomp-analysis (<< 0.6.4) Replaces: libcoq-mathcomp-analysis (<< 0.6.4) Provides: libcoq-mathcomp-classical-eoey0 Section: ocaml Priority: optional Homepage: https://github.com/math-comp/analysis Description: classical logic extension for Mathematical Components This package provides an extension for work with classical logic within the Coq proof-assistant using the Mathematical Components library. . 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:52 ./ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/ -rw-r--r-- root/root 560 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/all_classical.glob -rw-r--r-- root/root 410 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/all_classical.v -rw-r--r-- root/root 1495 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/all_classical.vo -rw-r--r-- root/root 243818 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/boolp.glob -rw-r--r-- root/root 36128 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/boolp.v -rw-r--r-- root/root 271694 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/boolp.vo -rw-r--r-- root/root 452849 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/cardinality.glob -rw-r--r-- root/root 55384 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/cardinality.v -rw-r--r-- root/root 600978 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/cardinality.vo -rw-r--r-- root/root 68921 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/classical_orders.glob -rw-r--r-- root/root 13506 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/classical_orders.v -rw-r--r-- root/root 242948 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/classical_orders.vo -rw-r--r-- root/root 1025178 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/classical_sets.glob -rw-r--r-- root/root 134426 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/classical_sets.v -rw-r--r-- root/root 1487142 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/classical_sets.vo -rw-r--r-- root/root 127817 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/contra.glob -rw-r--r-- root/root 49591 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/contra.v -rw-r--r-- root/root 126693 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/contra.vo -rw-r--r-- root/root 363673 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/filter.glob -rw-r--r-- root/root 68688 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/filter.v -rw-r--r-- root/root 681259 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/filter.vo -rw-r--r-- root/root 246105 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/fsbigop.glob -rw-r--r-- root/root 22868 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/fsbigop.v -rw-r--r-- root/root 203222 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/fsbigop.vo -rw-r--r-- root/root 892613 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/functions.glob -rw-r--r-- root/root 107122 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/functions.v -rw-r--r-- root/root 4331971 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/functions.vo -rw-r--r-- root/root 166772 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/mathcomp_extra.glob -rw-r--r-- root/root 20063 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/mathcomp_extra.v -rw-r--r-- root/root 187978 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/mathcomp_extra.vo -rw-r--r-- root/root 257307 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/set_interval.glob -rw-r--r-- root/root 30561 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/set_interval.v -rw-r--r-- root/root 494317 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/set_interval.vo -rw-r--r-- root/root 78712 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/wochoice.glob -rw-r--r-- root/root 18609 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/wochoice.v -rw-r--r-- root/root 178337 2025-01-15 15:52 ./usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/user-contrib/mathcomp/classical/wochoice.vo drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/share/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/share/doc/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./usr/share/doc/libcoq-mathcomp-classical/ -rw-r--r-- root/root 1306 2025-01-15 15:52 ./usr/share/doc/libcoq-mathcomp-classical/changelog.Debian.gz -rw-r--r-- root/root 67337 2024-12-18 23:35 ./usr/share/doc/libcoq-mathcomp-classical/changelog.gz -rw-r--r-- root/root 22511 2024-12-26 09:07 ./usr/share/doc/libcoq-mathcomp-classical/copyright drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/lib/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/lib/coq/ drwxr-xr-x root/root 0 2025-01-15 15:52 ./var/lib/coq/md5sums/ -rw-r--r-- root/root 5 2025-01-15 15:52 ./var/lib/coq/md5sums/libcoq-mathcomp-classical.checksum +------------------------------------------------------------------------------+ | Post Build Wed, 15 Jan 2025 16:09:18 +0000 | +------------------------------------------------------------------------------+ +------------------------------------------------------------------------------+ | Cleanup Wed, 15 Jan 2025 16:09:18 +0000 | +------------------------------------------------------------------------------+ Purging /build/reproducible-path Not cleaning session: cloned chroot in use +------------------------------------------------------------------------------+ | Summary Wed, 15 Jan 2025 16:09:18 +0000 | +------------------------------------------------------------------------------+ Build Architecture: amd64 Build Type: full Build-Space: 260836 Build-Time: 841 Distribution: unstable Host Architecture: amd64 Install-Time: 138 Job: /tmp/tmp.ben.transition-scripts.aj4eFnelIL/mathcomp-analysis_1.8.0-1+ocaml1.dsc Machine Architecture: amd64 Package: mathcomp-analysis Package-Time: 989 Source-Version: 1.8.0-1+ocaml1 Space: 260836 Status: successful Version: 1.8.0-1+ocaml1 -------------------------------------------------------------------------------- Finished at 2025-01-15T16:09:16Z Build needed 00:16:29, 260836k disk space