Tue Mar 4 11:27:41 UTC 2025 I: starting to build coq-unicoq/unstable/amd64 on jenkins on '2025-03-04 11:27'
Tue Mar 4 11:27:41 UTC 2025 I: The jenkins build log is/was available at https://jenkins.debian.net/userContent/reproducible/debian/build_service/amd64_26/33427/console.log
Tue Mar 4 11:27:41 UTC 2025 I: Downloading source for unstable/coq-unicoq=1.6-8.20-1
--2025-03-04 11:27:42-- http://deb.debian.org/debian/pool/main/c/coq-unicoq/coq-unicoq_1.6-8.20-1.dsc
Connecting to 46.16.76.132:3128... connected.
Proxy request sent, awaiting response... 200 OK
Length: 2094 (2.0K) [text/prs.lines.tag]
Saving to: ‘coq-unicoq_1.6-8.20-1.dsc’
0K .. 100% 251M=0s
2025-03-04 11:27:42 (251 MB/s) - ‘coq-unicoq_1.6-8.20-1.dsc’ saved [2094/2094]
Tue Mar 4 11:27:42 UTC 2025 I: coq-unicoq_1.6-8.20-1.dsc
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512
Format: 3.0 (quilt)
Source: coq-unicoq
Binary: libcoq-unicoq
Architecture: any
Version: 1.6-8.20-1
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders: Julien Puydt <jpuydt@debian.org>
Homepage: https://github.com/unicoq/unicoq/
Standards-Version: 4.7.0
Vcs-Browser: https://salsa.debian.org/ocaml-team/coq-unicoq
Vcs-Git: https://salsa.debian.org/ocaml-team/coq-unicoq.git
Testsuite: autopkgtest
Testsuite-Triggers: coq
Build-Depends: coq (>= 8.18), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib
Package-List:
libcoq-unicoq deb ocaml optional arch=any
Checksums-Sha1:
053e09086d85d7561790794982e17e4aa411c4b7 593674 coq-unicoq_1.6-8.20.orig.tar.gz
c2028714199f0622c612e437a8a10264b084b52d 2720 coq-unicoq_1.6-8.20-1.debian.tar.xz
Checksums-Sha256:
df81479e2292a44a0f300e38c49239d92d9a9df32f825aa0abf213f490bd5a7d 593674 coq-unicoq_1.6-8.20.orig.tar.gz
c58299af6e9dfaead46567d4b1bbb65d3c464a9a28afcfc1d4c73e89da8d0e5e 2720 coq-unicoq_1.6-8.20-1.debian.tar.xz
Files:
1c2a90a1a5c2652e77472d1498520367 593674 coq-unicoq_1.6-8.20.orig.tar.gz
af608f57b7230f12dec2608795645eac 2720 coq-unicoq_1.6-8.20-1.debian.tar.xz
-----BEGIN PGP SIGNATURE-----
iQJGBAEBCgAwFiEEgS7v2KP7pKzk3xFLBMU71/4DBVEFAmdB7xsSHGpwdXlkdEBk
ZWJpYW4ub3JnAAoJEATFO9f+AwVRbcMP/iPJzMvck2usX4Cnr0pVEXWpKuAKTxdA
NYTYHO0uolETXZnD/XqnCW93juLlCVVPR5TywD9ROFkzXAaiMpYC6Epfau/lYj3E
fZs1gQ1qKjNIVhb6CnnpLBe/Cc47tHatOAcZnHVZpWZKFCMEd5sRU1fOZL0sWU59
ZcYxLioYMLm+qGrgAyq0YO90KXRDCSbryUSxOl6+hJV2Ck3hsQ9jzg68a3tVLNLl
Fzom1xoBrl6SqmqY5A6W21e7CN6oxbdwmAIwFTcEPB0CpfNRJfrkBO66fMKlxNNC
j/dkRfga3cl0AhlqulPAICzv2J3gl1hqE9c1rJA9h0V2xYd1Uzl4oQ9MqnG9zin4
wwCYOvzRmJCqQsxxg5ooMXXjRPiVieuwDn1NBVY1na7YEGRtwVTNnDJwaFTmQYJ4
ncvM98Z7XnAREedsO5qsNuvZT5dP0Dd0PaZ2PBUs+f2WNkvp30GQz4GvXeAAT2xO
4kswZLD9ywEptOqhx1YecPY9bMu6T1veo2IWOjHs6DJlg+Qf7vbe/p+IWOWxLceF
ZMyv819yYxlQnDUaq+kSpbtu1Vaoh7xprafPIAFIPhTXS4gBXkKIL0fDrFctWPx3
AkZO182zq69pzwzKz2wSEpephkAAzyDPtj2dW+DZEKqu5CBfVd9Za9SR2N/Wszve
0gZSII1ybLF4
=gyqW
-----END PGP SIGNATURE-----
Tue Mar 4 11:27:42 UTC 2025 I: Checking whether the package is not for us
Tue Mar 4 11:27:42 UTC 2025 I: Starting 1st build on remote node ionos5-amd64.debian.net.
Tue Mar 4 11:27:42 UTC 2025 I: Preparing to do remote build '1' on ionos5-amd64.debian.net.
Tue Mar 4 11:29:59 UTC 2025 I: Deleting $TMPDIR on ionos5-amd64.debian.net.
I: pbuilder: network access will be disabled during build
I: Current time: Mon Apr 6 05:50:43 -12 2026
I: pbuilder-time-stamp: 1775497843
I: Building the build Environment
I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz]
I: copying local configuration
W: --override-config is not set; not updating apt.conf Read the manpage for details.
I: mounting /proc filesystem
I: mounting /sys filesystem
I: creating /{dev,run}/shm
I: mounting /dev/pts filesystem
I: redirecting /dev/ptmx to /dev/pts/ptmx
I: policy-rc.d already exists
I: Copying source file
I: copying [coq-unicoq_1.6-8.20-1.dsc]
I: copying [./coq-unicoq_1.6-8.20.orig.tar.gz]
I: copying [./coq-unicoq_1.6-8.20-1.debian.tar.xz]
I: Extracting source
dpkg-source: warning: cannot verify inline signature for ./coq-unicoq_1.6-8.20-1.dsc: unsupported subcommand
dpkg-source: info: extracting coq-unicoq in coq-unicoq-1.6-8.20
dpkg-source: info: unpacking coq-unicoq_1.6-8.20.orig.tar.gz
dpkg-source: info: unpacking coq-unicoq_1.6-8.20-1.debian.tar.xz
I: Not using root during the build.
I: Installing the build-deps
I: user script /srv/workspace/pbuilder/2185331/tmp/hooks/D02_print_environment starting
I: set
BUILDDIR='/build/reproducible-path'
BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other'
BUILDUSERNAME='pbuilder1'
BUILD_ARCH='amd64'
DEBIAN_FRONTEND='noninteractive'
DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=42 '
DISTRIBUTION='unstable'
HOME='/root'
HOST_ARCH='amd64'
IFS='
'
INVOCATION_ID='09cb28e3c2e0420581cb9e03efcab52b'
LANG='C'
LANGUAGE='en_US:en'
LC_ALL='C'
MAIL='/var/mail/root'
OPTIND='1'
PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games'
PBCURRENTCOMMANDLINEOPERATION='build'
PBUILDER_OPERATION='build'
PBUILDER_PKGDATADIR='/usr/share/pbuilder'
PBUILDER_PKGLIBDIR='/usr/lib/pbuilder'
PBUILDER_SYSCONFDIR='/etc'
PPID='2185331'
PS1='# '
PS2='> '
PS4='+ '
PWD='/'
SHELL='/bin/bash'
SHLVL='2'
SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.3xwkdLWH/pbuilderrc_OSUa --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.3xwkdLWH/b1 --logfile b1/build.log coq-unicoq_1.6-8.20-1.dsc'
SUDO_GID='110'
SUDO_UID='105'
SUDO_USER='jenkins'
TERM='unknown'
TZ='/usr/share/zoneinfo/Etc/GMT+12'
USER='root'
_='/usr/bin/systemd-run'
http_proxy='http://213.165.73.152:3128'
I: uname -a
Linux ionos5-amd64 6.12.12+bpo-amd64 #1 SMP PREEMPT_DYNAMIC Debian 6.12.12-1~bpo12+1 (2025-02-23) x86_64 GNU/Linux
I: ls -l /bin
lrwxrwxrwx 1 root root 7 Nov 22 2024 /bin -> usr/bin
I: user script /srv/workspace/pbuilder/2185331/tmp/hooks/D02_print_environment finished
-> Attempting to satisfy build-dependencies
-> Creating pbuilder-satisfydepends-dummy package
Package: pbuilder-satisfydepends-dummy
Version: 0.invalid.0
Architecture: amd64
Maintainer: Debian Pbuilder Team <pbuilder-maint@lists.alioth.debian.org>
Description: Dummy package to satisfy dependencies with aptitude - created by pbuilder
This package was created automatically by pbuilder to satisfy the
build-dependencies of the package being currently built.
Depends: coq (>= 8.18), debhelper-compat (= 13), dh-coq, dh-ocaml, libcoq-core-ocaml-dev, libcoq-stdlib
dpkg-deb: building package 'pbuilder-satisfydepends-dummy' in '/tmp/satisfydepends-aptitude/pbuilder-satisfydepends-dummy.deb'.
Selecting previously unselected package pbuilder-satisfydepends-dummy.
(Reading database ... 19783 files and directories currently installed.)
Preparing to unpack .../pbuilder-satisfydepends-dummy.deb ...
Unpacking pbuilder-satisfydepends-dummy (0.invalid.0) ...
dpkg: pbuilder-satisfydepends-dummy: dependency problems, but configuring anyway as you requested:
pbuilder-satisfydepends-dummy depends on coq (>= 8.18); however:
Package coq is not installed.
pbuilder-satisfydepends-dummy depends on debhelper-compat (= 13); however:
Package debhelper-compat is not installed.
pbuilder-satisfydepends-dummy depends on dh-coq; however:
Package dh-coq is not installed.
pbuilder-satisfydepends-dummy depends on dh-ocaml; however:
Package dh-ocaml is not installed.
pbuilder-satisfydepends-dummy depends on libcoq-core-ocaml-dev; however:
Package libcoq-core-ocaml-dev is not installed.
pbuilder-satisfydepends-dummy depends on libcoq-stdlib; however:
Package libcoq-stdlib is not installed.
Setting up pbuilder-satisfydepends-dummy (0.invalid.0) ...
Reading package lists...
Building dependency tree...
Reading state information...
Initializing package states...
Writing extended state information...
Building tag database...
pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0)
pbuilder-satisfydepends-dummy is already installed at the requested version (0.invalid.0)
The following NEW packages will be installed:
autoconf{a} automake{a} autopoint{a} autotools-dev{a} bsdextrautils{a} debhelper{a} dh-autoreconf{a} dh-coq{a} dh-ocaml{a} dh-strip-nondeterminism{a} dwz{a} file{a} gettext{a} gettext-base{a} groff-base{a} intltool-debian{a} libarchive-zip-perl{a} libconfig-tiny-perl{a} libcoq-stdlib{a} libdebhelper-perl{a} libelf1t64{a} libfile-stripnondeterminism-perl{a} libicu72{a} libmagic-mgc{a} libmagic1t64{a} libpipeline1{a} libtool{a} libuchardet0{a} libunistring5{a} libxml2{a} m4{a} man-db{a} po-debconf{a} sensible-utils{a}
The following packages are RECOMMENDED but will NOT be installed:
curl libarchive-cpio-perl libltdl-dev libmail-sendmail-perl lynx ocaml wget
0 packages upgraded, 34 newly installed, 0 to remove and 0 not upgraded.
Need to get 44.2 MB of archives. After unpacking 228 MB will be used.
The following packages have unmet dependencies:
pbuilder-satisfydepends-dummy : Depends: coq (>= 8.18) but it is not installable
Depends: libcoq-core-ocaml-dev but it is not installable
The following actions will resolve these dependencies:
Install the following packages:
1) coq [8.20.1+dfsg-1 (unstable)]
2) libcompiler-libs-ocaml-dev [5.3.0-2 (unstable)]
3) libcoq-core-ocaml [8.20.1+dfsg-1 (unstable)]
4) libcoq-core-ocaml-dev [8.20.1+dfsg-1 (unstable)]
5) libexpat1 [2.6.4-1 (unstable)]
6) libffi8 [3.4.7-1 (unstable)]
7) libfindlib-ocaml [1.9.8-1 (unstable)]
8) libfindlib-ocaml-dev [1.9.8-1 (unstable)]
9) libgmp-dev [2:6.3.0+dfsg-3 (unstable)]
10) libgmp3-dev [2:6.3.0+dfsg-3 (unstable)]
11) libgmpxx4ldbl [2:6.3.0+dfsg-3 (unstable)]
12) libncurses-dev [6.5+20250216-1 (unstable)]
13) libncurses6 [6.5+20250216-1 (unstable)]
14) libpython3-stdlib [3.13.2-1 (unstable)]
15) libpython3.13-minimal [3.13.2-1 (unstable)]
16) libpython3.13-stdlib [3.13.2-1 (unstable)]
17) libreadline8t64 [8.2-6 (unstable)]
18) libstdlib-ocaml [5.3.0-2 (unstable)]
19) libstdlib-ocaml-dev [5.3.0-2 (unstable)]
20) libzarith-ocaml [1.14-1+b1 (unstable)]
21) libzarith-ocaml-dev [1.14-1+b1 (unstable)]
22) libzstd-dev [1.5.6+dfsg-2 (unstable)]
23) media-types [12.0.0 (unstable)]
24) netbase [6.4 (unstable)]
25) ocaml [5.3.0-2 (unstable)]
26) ocaml-base [5.3.0-2 (unstable)]
27) ocaml-findlib [1.9.8-1 (unstable)]
28) ocaml-interp [5.3.0-2 (unstable)]
29) python3 [3.13.2-1 (unstable)]
30) python3-minimal [3.13.2-1 (unstable)]
31) python3.13 [3.13.2-1 (unstable)]
32) python3.13-minimal [3.13.2-1 (unstable)]
33) readline-common [8.2-6 (unstable)]
34) tzdata [2025a-2 (unstable)]
The following NEW packages will be installed:
autoconf{a} automake{a} autopoint{a} autotools-dev{a} bsdextrautils{a} coq{a} debhelper{a} dh-autoreconf{a} dh-coq{a} dh-ocaml{a} dh-strip-nondeterminism{a} dwz{a} file{a} gettext{a} gettext-base{a} groff-base{a} intltool-debian{a} libarchive-zip-perl{a} libcompiler-libs-ocaml-dev{a} libconfig-tiny-perl{a} libcoq-core-ocaml{a} libcoq-core-ocaml-dev{a} libcoq-stdlib{a} libdebhelper-perl{a} libelf1t64{a} libexpat1{a} libffi8{a} libfile-stripnondeterminism-perl{a} libfindlib-ocaml{a} libfindlib-ocaml-dev{a} libgmp-dev{a} libgmp3-dev{a} libgmpxx4ldbl{a} libicu72{a} libmagic-mgc{a} libmagic1t64{a} libncurses-dev{a} libncurses6{a} libpipeline1{a} libpython3-stdlib{a} libpython3.13-minimal{a} libpython3.13-stdlib{a} libreadline8t64{a} libstdlib-ocaml{a} libstdlib-ocaml-dev{a} libtool{a} libuchardet0{a} libunistring5{a} libxml2{a} libzarith-ocaml{a} libzarith-ocaml-dev{a} libzstd-dev{a} m4{a} man-db{a} media-types{a} netbase{a} ocaml{a} ocaml-base{a} ocaml-findlib{a} ocaml-interp{a} po-debconf{a} python3{a} python3-minimal{a} python3.13{a} python3.13-minimal{a} readline-common{a} sensible-utils{a} tzdata{a}
The following packages are RECOMMENDED but will NOT be installed:
ca-certificates curl ledit libarchive-cpio-perl libgpm2 libltdl-dev libmail-sendmail-perl lynx ocaml-man rlfe rlwrap wget
0 packages upgraded, 68 newly installed, 0 to remove and 0 not upgraded.
Need to get 301 MB of archives. After unpacking 963 MB will be used.
Writing extended state information...
Get: 1 http://deb.debian.org/debian unstable/main amd64 libpython3.13-minimal amd64 3.13.2-1 [859 kB]
Get: 2 http://deb.debian.org/debian unstable/main amd64 libexpat1 amd64 2.6.4-1 [106 kB]
Get: 3 http://deb.debian.org/debian unstable/main amd64 python3.13-minimal amd64 3.13.2-1 [2205 kB]
Get: 4 http://deb.debian.org/debian unstable/main amd64 python3-minimal amd64 3.13.2-1 [27.1 kB]
Get: 5 http://deb.debian.org/debian unstable/main amd64 media-types all 12.0.0 [28.9 kB]
Get: 6 http://deb.debian.org/debian unstable/main amd64 netbase all 6.4 [12.8 kB]
Get: 7 http://deb.debian.org/debian unstable/main amd64 tzdata all 2025a-2 [259 kB]
Get: 8 http://deb.debian.org/debian unstable/main amd64 libffi8 amd64 3.4.7-1 [23.9 kB]
Get: 9 http://deb.debian.org/debian unstable/main amd64 readline-common all 8.2-6 [69.4 kB]
Get: 10 http://deb.debian.org/debian unstable/main amd64 libreadline8t64 amd64 8.2-6 [169 kB]
Get: 11 http://deb.debian.org/debian unstable/main amd64 libpython3.13-stdlib amd64 3.13.2-1 [1979 kB]
Get: 12 http://deb.debian.org/debian unstable/main amd64 python3.13 amd64 3.13.2-1 [745 kB]
Get: 13 http://deb.debian.org/debian unstable/main amd64 libpython3-stdlib amd64 3.13.2-1 [10.0 kB]
Get: 14 http://deb.debian.org/debian unstable/main amd64 python3 amd64 3.13.2-1 [28.1 kB]
Get: 15 http://deb.debian.org/debian unstable/main amd64 sensible-utils all 0.0.24 [24.8 kB]
Get: 16 http://deb.debian.org/debian unstable/main amd64 libmagic-mgc amd64 1:5.45-3+b1 [314 kB]
Get: 17 http://deb.debian.org/debian unstable/main amd64 libmagic1t64 amd64 1:5.45-3+b1 [108 kB]
Get: 18 http://deb.debian.org/debian unstable/main amd64 file amd64 1:5.45-3+b1 [43.3 kB]
Get: 19 http://deb.debian.org/debian unstable/main amd64 gettext-base amd64 0.23.1-1 [243 kB]
Get: 20 http://deb.debian.org/debian unstable/main amd64 libuchardet0 amd64 0.0.8-1+b2 [68.9 kB]
Get: 21 http://deb.debian.org/debian unstable/main amd64 groff-base amd64 1.23.0-7 [1185 kB]
Get: 22 http://deb.debian.org/debian unstable/main amd64 bsdextrautils amd64 2.40.4-5 [92.4 kB]
Get: 23 http://deb.debian.org/debian unstable/main amd64 libpipeline1 amd64 1.5.8-1 [42.0 kB]
Get: 24 http://deb.debian.org/debian unstable/main amd64 man-db amd64 2.13.0-1 [1420 kB]
Get: 25 http://deb.debian.org/debian unstable/main amd64 m4 amd64 1.4.19-5 [294 kB]
Get: 26 http://deb.debian.org/debian unstable/main amd64 autoconf all 2.72-3 [493 kB]
Get: 27 http://deb.debian.org/debian unstable/main amd64 autotools-dev all 20220109.1 [51.6 kB]
Get: 28 http://deb.debian.org/debian unstable/main amd64 automake all 1:1.17-3 [862 kB]
Get: 29 http://deb.debian.org/debian unstable/main amd64 autopoint all 0.23.1-1 [770 kB]
Get: 30 http://deb.debian.org/debian unstable/main amd64 libcoq-stdlib amd64 8.20.1+dfsg-1 [23.5 MB]
Get: 31 http://deb.debian.org/debian unstable/main amd64 libstdlib-ocaml amd64 5.3.0-2 [605 kB]
Get: 32 http://deb.debian.org/debian unstable/main amd64 ocaml-base amd64 5.3.0-2 [495 kB]
Get: 33 http://deb.debian.org/debian unstable/main amd64 libfindlib-ocaml amd64 1.9.8-1 [214 kB]
Get: 34 http://deb.debian.org/debian unstable/main amd64 libzarith-ocaml amd64 1.14-1+b1 [117 kB]
Get: 35 http://deb.debian.org/debian unstable/main amd64 libcoq-core-ocaml amd64 8.20.1+dfsg-1 [26.0 MB]
Get: 36 http://deb.debian.org/debian unstable/main amd64 libstdlib-ocaml-dev amd64 5.3.0-2 [7886 kB]
Get: 37 http://deb.debian.org/debian unstable/main amd64 libcompiler-libs-ocaml-dev amd64 5.3.0-2 [48.2 MB]
Get: 38 http://deb.debian.org/debian unstable/main amd64 ocaml-interp amd64 5.3.0-2 [7106 kB]
Get: 39 http://deb.debian.org/debian unstable/main amd64 libncurses6 amd64 6.5+20250216-1 [105 kB]
Get: 40 http://deb.debian.org/debian unstable/main amd64 libncurses-dev amd64 6.5+20250216-1 [353 kB]
Get: 41 http://deb.debian.org/debian unstable/main amd64 libzstd-dev amd64 1.5.6+dfsg-2 [365 kB]
Get: 42 http://deb.debian.org/debian unstable/main amd64 ocaml amd64 5.3.0-2 [18.0 MB]
Get: 43 http://deb.debian.org/debian unstable/main amd64 ocaml-findlib amd64 1.9.8-1 [584 kB]
Get: 44 http://deb.debian.org/debian unstable/main amd64 coq amd64 8.20.1+dfsg-1 [70.2 MB]
Get: 45 http://deb.debian.org/debian unstable/main amd64 libdebhelper-perl all 13.24.1 [90.9 kB]
Get: 46 http://deb.debian.org/debian unstable/main amd64 libtool all 2.5.4-3 [539 kB]
Get: 47 http://deb.debian.org/debian unstable/main amd64 dh-autoreconf all 20 [17.1 kB]
Get: 48 http://deb.debian.org/debian unstable/main amd64 libarchive-zip-perl all 1.68-1 [104 kB]
Get: 49 http://deb.debian.org/debian unstable/main amd64 libfile-stripnondeterminism-perl all 1.14.1-2 [19.7 kB]
Get: 50 http://deb.debian.org/debian unstable/main amd64 dh-strip-nondeterminism all 1.14.1-2 [8620 B]
Get: 51 http://deb.debian.org/debian unstable/main amd64 libelf1t64 amd64 0.192-4 [189 kB]
Get: 52 http://deb.debian.org/debian unstable/main amd64 dwz amd64 0.15-1+b1 [110 kB]
Get: 53 http://deb.debian.org/debian unstable/main amd64 libunistring5 amd64 1.3-1 [476 kB]
Get: 54 http://deb.debian.org/debian unstable/main amd64 libicu72 amd64 72.1-6 [9421 kB]
Get: 55 http://deb.debian.org/debian unstable/main amd64 libxml2 amd64 2.12.7+dfsg+really2.9.14-0.2+b2 [699 kB]
Get: 56 http://deb.debian.org/debian unstable/main amd64 gettext amd64 0.23.1-1 [1680 kB]
Get: 57 http://deb.debian.org/debian unstable/main amd64 intltool-debian all 0.35.0+20060710.6 [22.9 kB]
Get: 58 http://deb.debian.org/debian unstable/main amd64 po-debconf all 1.0.21+nmu1 [248 kB]
Get: 59 http://deb.debian.org/debian unstable/main amd64 debhelper all 13.24.1 [920 kB]
Get: 60 http://deb.debian.org/debian unstable/main amd64 dh-coq all 0.14 [6956 B]
Get: 61 http://deb.debian.org/debian unstable/main amd64 libconfig-tiny-perl all 2.30-1 [18.9 kB]
Get: 62 http://deb.debian.org/debian unstable/main amd64 dh-ocaml all 2.4 [62.9 kB]
Get: 63 http://deb.debian.org/debian unstable/main amd64 libfindlib-ocaml-dev amd64 1.9.8-1 [179 kB]
Get: 64 http://deb.debian.org/debian unstable/main amd64 libgmpxx4ldbl amd64 2:6.3.0+dfsg-3 [329 kB]
Get: 65 http://deb.debian.org/debian unstable/main amd64 libgmp-dev amd64 2:6.3.0+dfsg-3 [642 kB]
Get: 66 http://deb.debian.org/debian unstable/main amd64 libgmp3-dev amd64 2:6.3.0+dfsg-3 [322 kB]
Get: 67 http://deb.debian.org/debian unstable/main amd64 libzarith-ocaml-dev amd64 1.14-1+b1 [143 kB]
Get: 68 http://deb.debian.org/debian unstable/main amd64 libcoq-core-ocaml-dev amd64 8.20.1+dfsg-1 [68.7 MB]
Fetched 301 MB in 14s (22.2 MB/s)
Preconfiguring packages ...
Selecting previously unselected package libpython3.13-minimal:amd64.
(Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 19783 files and directories currently installed.)
Preparing to unpack .../libpython3.13-minimal_3.13.2-1_amd64.deb ...
Unpacking libpython3.13-minimal:amd64 (3.13.2-1) ...
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.2-1_amd64.deb ...
Unpacking python3.13-minimal (3.13.2-1) ...
Setting up libpython3.13-minimal:amd64 (3.13.2-1) ...
Setting up libexpat1:amd64 (2.6.4-1) ...
Setting up python3.13-minimal (3.13.2-1) ...
Selecting previously unselected package python3-minimal.
(Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 20117 files and directories currently installed.)
Preparing to unpack .../0-python3-minimal_3.13.2-1_amd64.deb ...
Unpacking python3-minimal (3.13.2-1) ...
Selecting previously unselected package media-types.
Preparing to unpack .../1-media-types_12.0.0_all.deb ...
Unpacking media-types (12.0.0) ...
Selecting previously unselected package netbase.
Preparing to unpack .../2-netbase_6.4_all.deb ...
Unpacking netbase (6.4) ...
Selecting previously unselected package tzdata.
Preparing to unpack .../3-tzdata_2025a-2_all.deb ...
Unpacking tzdata (2025a-2) ...
Selecting previously unselected package libffi8:amd64.
Preparing to unpack .../4-libffi8_3.4.7-1_amd64.deb ...
Unpacking libffi8:amd64 (3.4.7-1) ...
Selecting previously unselected package readline-common.
Preparing to unpack .../5-readline-common_8.2-6_all.deb ...
Unpacking readline-common (8.2-6) ...
Selecting previously unselected package libreadline8t64:amd64.
Preparing to unpack .../6-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 libpython3.13-stdlib:amd64.
Preparing to unpack .../7-libpython3.13-stdlib_3.13.2-1_amd64.deb ...
Unpacking libpython3.13-stdlib:amd64 (3.13.2-1) ...
Selecting previously unselected package python3.13.
Preparing to unpack .../8-python3.13_3.13.2-1_amd64.deb ...
Unpacking python3.13 (3.13.2-1) ...
Selecting previously unselected package libpython3-stdlib:amd64.
Preparing to unpack .../9-libpython3-stdlib_3.13.2-1_amd64.deb ...
Unpacking libpython3-stdlib:amd64 (3.13.2-1) ...
Setting up python3-minimal (3.13.2-1) ...
Selecting previously unselected package python3.
(Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 21127 files and directories currently installed.)
Preparing to unpack .../00-python3_3.13.2-1_amd64.deb ...
Unpacking python3 (3.13.2-1) ...
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.23.1-1_amd64.deb ...
Unpacking gettext-base (0.23.1-1) ...
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-5_amd64.deb ...
Unpacking bsdextrautils (2.40.4-5) ...
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.17-3_all.deb ...
Unpacking automake (1:1.17-3) ...
Selecting previously unselected package autopoint.
Preparing to unpack .../15-autopoint_0.23.1-1_all.deb ...
Unpacking autopoint (0.23.1-1) ...
Selecting previously unselected package libcoq-stdlib.
Preparing to unpack .../16-libcoq-stdlib_8.20.1+dfsg-1_amd64.deb ...
Unpacking libcoq-stdlib (8.20.1+dfsg-1) ...
Selecting previously unselected package libstdlib-ocaml.
Preparing to unpack .../17-libstdlib-ocaml_5.3.0-2_amd64.deb ...
Unpacking libstdlib-ocaml (5.3.0-2) ...
Selecting previously unselected package ocaml-base.
Preparing to unpack .../18-ocaml-base_5.3.0-2_amd64.deb ...
Unpacking ocaml-base (5.3.0-2) ...
Selecting previously unselected package libfindlib-ocaml.
Preparing to unpack .../19-libfindlib-ocaml_1.9.8-1_amd64.deb ...
Unpacking libfindlib-ocaml (1.9.8-1) ...
Selecting previously unselected package libzarith-ocaml.
Preparing to unpack .../20-libzarith-ocaml_1.14-1+b1_amd64.deb ...
Unpacking libzarith-ocaml (1.14-1+b1) ...
Selecting previously unselected package libcoq-core-ocaml.
Preparing to unpack .../21-libcoq-core-ocaml_8.20.1+dfsg-1_amd64.deb ...
Unpacking libcoq-core-ocaml (8.20.1+dfsg-1) ...
Selecting previously unselected package libstdlib-ocaml-dev.
Preparing to unpack .../22-libstdlib-ocaml-dev_5.3.0-2_amd64.deb ...
Unpacking libstdlib-ocaml-dev (5.3.0-2) ...
Selecting previously unselected package libcompiler-libs-ocaml-dev.
Preparing to unpack .../23-libcompiler-libs-ocaml-dev_5.3.0-2_amd64.deb ...
Unpacking libcompiler-libs-ocaml-dev (5.3.0-2) ...
Selecting previously unselected package ocaml-interp.
Preparing to unpack .../24-ocaml-interp_5.3.0-2_amd64.deb ...
Unpacking ocaml-interp (5.3.0-2) ...
Selecting previously unselected package libncurses6:amd64.
Preparing to unpack .../25-libncurses6_6.5+20250216-1_amd64.deb ...
Unpacking libncurses6:amd64 (6.5+20250216-1) ...
Selecting previously unselected package libncurses-dev:amd64.
Preparing to unpack .../26-libncurses-dev_6.5+20250216-1_amd64.deb ...
Unpacking libncurses-dev:amd64 (6.5+20250216-1) ...
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-2_amd64.deb ...
Unpacking ocaml (5.3.0-2) ...
Selecting previously unselected package ocaml-findlib.
Preparing to unpack .../29-ocaml-findlib_1.9.8-1_amd64.deb ...
Unpacking ocaml-findlib (1.9.8-1) ...
Selecting previously unselected package coq.
Preparing to unpack .../30-coq_8.20.1+dfsg-1_amd64.deb ...
Unpacking coq (8.20.1+dfsg-1) ...
Selecting previously unselected package libdebhelper-perl.
Preparing to unpack .../31-libdebhelper-perl_13.24.1_all.deb ...
Unpacking libdebhelper-perl (13.24.1) ...
Selecting previously unselected package libtool.
Preparing to unpack .../32-libtool_2.5.4-3_all.deb ...
Unpacking libtool (2.5.4-3) ...
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.1-2_all.deb ...
Unpacking libfile-stripnondeterminism-perl (1.14.1-2) ...
Selecting previously unselected package dh-strip-nondeterminism.
Preparing to unpack .../36-dh-strip-nondeterminism_1.14.1-2_all.deb ...
Unpacking dh-strip-nondeterminism (1.14.1-2) ...
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+b2_amd64.deb ...
Unpacking libxml2:amd64 (2.12.7+dfsg+really2.9.14-0.2+b2) ...
Selecting previously unselected package gettext.
Preparing to unpack .../42-gettext_0.23.1-1_amd64.deb ...
Unpacking gettext (0.23.1-1) ...
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.24.1_all.deb ...
Unpacking debhelper (13.24.1) ...
Selecting previously unselected package dh-coq.
Preparing to unpack .../46-dh-coq_0.14_all.deb ...
Unpacking dh-coq (0.14) ...
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_all.deb ...
Unpacking dh-ocaml (2.4) ...
Selecting previously unselected package libfindlib-ocaml-dev.
Preparing to unpack .../49-libfindlib-ocaml-dev_1.9.8-1_amd64.deb ...
Unpacking libfindlib-ocaml-dev (1.9.8-1) ...
Selecting previously unselected package libgmpxx4ldbl:amd64.
Preparing to unpack .../50-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 .../51-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 .../52-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 .../53-libzarith-ocaml-dev_1.14-1+b1_amd64.deb ...
Unpacking libzarith-ocaml-dev (1.14-1+b1) ...
Selecting previously unselected package libcoq-core-ocaml-dev.
Preparing to unpack .../54-libcoq-core-ocaml-dev_8.20.1+dfsg-1_amd64.deb ...
Unpacking libcoq-core-ocaml-dev (8.20.1+dfsg-1) ...
Setting up media-types (12.0.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-5) ...
Setting up libmagic-mgc (1:5.45-3+b1) ...
Setting up dh-coq (0.14) ...
Setting up libarchive-zip-perl (1.68-1) ...
Setting up libdebhelper-perl (13.24.1) ...
Setting up libmagic1t64:amd64 (1:5.45-3+b1) ...
Setting up gettext-base (0.23.1-1) ...
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 libelf1t64:amd64 (0.192-4) ...
Setting up tzdata (2025a-2) ...
Current default time zone: 'Etc/UTC'
Local time is now: Mon Apr 6 17:52:32 UTC 2026.
Universal Time is now: Mon Apr 6 17:52:32 UTC 2026.
Run 'dpkg-reconfigure tzdata' if you wish to change it.
Setting up autotools-dev (20220109.1) ...
Setting up libcoq-stdlib (8.20.1+dfsg-1) ...
Setting up libgmpxx4ldbl:amd64 (2:6.3.0+dfsg-3) ...
Setting up libncurses6:amd64 (6.5+20250216-1) ...
Setting up libstdlib-ocaml (5.3.0-2) ...
Setting up libunistring5:amd64 (1.3-1) ...
Setting up autopoint (0.23.1-1) ...
Setting up ocaml-base (5.3.0-2) ...
Setting up autoconf (2.72-3) ...
Setting up libffi8:amd64 (3.4.7-1) ...
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+b2) ...
Setting up automake (1:1.17-3) ...
update-alternatives: using /usr/bin/automake-1.17 to provide /usr/bin/automake (automake) in auto mode
Setting up libfile-stripnondeterminism-perl (1.14.1-2) ...
Setting up libncurses-dev:amd64 (6.5+20250216-1) ...
Setting up gettext (0.23.1-1) ...
Setting up libgmp-dev:amd64 (2:6.3.0+dfsg-3) ...
Setting up libtool (2.5.4-3) ...
Setting up libstdlib-ocaml-dev (5.3.0-2) ...
Setting up dh-ocaml (2.4) ...
Setting up libfindlib-ocaml (1.9.8-1) ...
Setting up libzarith-ocaml (1.14-1+b1) ...
Setting up intltool-debian (0.35.0+20060710.6) ...
Setting up dh-autoreconf (20) ...
Setting up libcompiler-libs-ocaml-dev (5.3.0-2) ...
Setting up ocaml-interp (5.3.0-2) ...
Setting up ocaml-findlib (1.9.8-1) ...
Setting up libreadline8t64:amd64 (8.2-6) ...
Setting up dh-strip-nondeterminism (1.14.1-2) ...
Setting up libcoq-core-ocaml (8.20.1+dfsg-1) ...
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.2-1) ...
Setting up libpython3-stdlib:amd64 (3.13.2-1) ...
Setting up python3.13 (3.13.2-1) ...
Setting up po-debconf (1.0.21+nmu1) ...
Setting up python3 (3.13.2-1) ...
Setting up ocaml (5.3.0-2) ...
Setting up man-db (2.13.0-1) ...
Not building database; man-db/auto-update is not 'true'.
Setting up libfindlib-ocaml-dev (1.9.8-1) ...
Setting up coq (8.20.1+dfsg-1) ...
Setting up libzarith-ocaml-dev (1.14-1+b1) ...
Setting up debhelper (13.24.1) ...
Setting up libcoq-core-ocaml-dev (8.20.1+dfsg-1) ...
Processing triggers for libc-bin (2.41-3) ...
Reading package lists...
Building dependency tree...
Reading state information...
Reading extended state information...
Initializing package states...
Writing extended state information...
Building tag database...
-> Finished parsing the build-deps
I: Building the package
I: Running cd /build/reproducible-path/coq-unicoq-1.6-8.20/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../coq-unicoq_1.6-8.20-1_source.changes
dpkg-buildpackage: info: source package coq-unicoq
dpkg-buildpackage: info: source version 1.6-8.20-1
dpkg-buildpackage: info: source distribution unstable
dpkg-buildpackage: info: source changed by Julien Puydt <jpuydt@debian.org>
dpkg-source --before-build .
dpkg-buildpackage: info: host architecture amd64
debian/rules clean
dh clean --with coq,ocaml
debian/rules override_dh_auto_clean
make[1]: Entering directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
if test -f Makefile; then \
make clean; \
fi
find . -name "*.aux" -delete
rm -f Makefile Makefile.conf src/META.coq-unicoq unif.tex
make[1]: Leaving directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
dh_ocamlclean
dh_clean
debian/rules binary
dh binary --with coq,ocaml
dh_update_autotools_config
dh_autoreconf
dh_ocamlinit
debian/rules override_dh_auto_configure
make[1]: Entering directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
coq_makefile -f _CoqProject -o Makefile
make[1]: Leaving directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
dh_auto_build
make -j42 "INSTALL=install --strip-program=true"
make[1]: Entering directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
COQPP src/unitactics.mlg
COQDEP VFILES
CAMLDEP src/unitactics.ml
CAMLDEP src/logger.ml
CAMLDEP src/munify.ml
OCAMLLIBDEP src/unicoq.mlpack
CAMLDEP src/logger.mli
CAMLDEP src/munify.mli
CAMLC -c src/logger.mli
CAMLOPT -c -for-pack Unicoq src/logger.ml
CAMLC -c src/munify.mli
CAMLOPT -c -for-pack Unicoq src/munify.ml
File "src/munify.ml", line 680, characters 8-32:
680 | Termops.global_of_constr sigma t1, l1
^^^^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Termops.global_of_constr
Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
File "src/munify.ml", line 700, characters 25-49:
700 | let c2,_ = Termops.global_of_constr sigma t2 in
^^^^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Termops.global_of_constr
Use [EConstr.destRef] instead (throws DestKO instead of Not_found).
File "src/munify.ml", line 1226, characters 38-52:
1226 | | Const (c1,_), Const (c2,_) when Constant.equal c1 c2 ->
^^^^^^^^^^^^^^
Alert deprecated: Names.Constant.equal
Use QConstant.equal
File "src/munify.ml", line 1239, characters 46-73:
1239 | | Proj (c1, _, t1), Proj (c2, _, t2) when Names.Projection.repr_equal c1 c2 ->
^^^^^^^^^^^^^^^^^^^^^^^^^^^
Alert deprecated: Names.Projection.repr_equal
Use an explicit projection of Repr
CAMLOPT -c -for-pack Unicoq src/unitactics.ml
CAMLOPT -pack -o src/unicoq.cmx
CAMLOPT -a -o src/unicoq.cmxa
CAMLOPT -shared -o src/unicoq.cmxs
COQC theories/Unicoq.v
COQC test-suite/munifytest.v
COQC test-suite/microtests.v
COQC test-suite/primitive.v
COQC test-suite/instantiate.v
COQC test-suite/timings.v
COQC test-suite/bug_41.v
COQC test-suite/bug_44.v
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)(let x := True in ?Goal)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
(0 = 0) =<= (?n x = 0) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
_(?n x) =?= 0 (Meta-Inst)
__(nat -> nat) =<= (nat -> nat) (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
_0 =?= 0 (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
inst1 = eq_refl
: (fun _ : nat => 0) x = 0
inst1 uses section variable x.
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(x = x) =<= (?n x = x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(?n x) =?= x (Meta-Inst)
_(?n x) =?= x (Meta-DelDeps)
__(?n x) =?= x (Meta-Inst)
___(nat -> nat) =<= (nat -> nat) (Reduce-Same)
_x =?= x (Reduce-Same)
inst2 = eq_refl
: (fun n : nat => n) x = x
inst2 uses section variable x.
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(x = x) =<= (?n x y z = x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(?n x y z) =?= x (Meta-Inst)
_(?n x y z) =?= x (Meta-DelDeps)
__(?n x y z) =?= x (Meta-Inst)
___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same)
_x =?= x (Reduce-Same)
inst3 = eq_refl
: (fun n _ _ : nat => n) x y z = x
inst3 uses section variables x y z.
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; y:=y; x0:=x; x1:=y\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} (Meta-Inst)
?T@\{x:=x; y:=y; z:=z; x0:=x; x1:=y; x2:=z\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(z = z) =<= (?n x y z = z) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(?n x y z) =?= z (Meta-Inst)
_(?n x y z) =?= z (Meta-DelDeps)
__(?n x y z) =?= z (Meta-Inst)STATS: 0 0
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
___(nat -> nat -> nat -> nat) =<= (nat -> nat -> nat -> nat) (Reduce-Same)
_z =?= z (Reduce-Same)
inst4 = eq_refl
: (fun _ _ n : nat => n) x y z = z
inst4 uses section variables x y z.
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same) OK
(nat -> nat) =<= nat (App-FO)
nat =<= nat (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same) ERR
(nat -> nat) =<= nat (App-FO)
nat =<= nat (Reduce-Same)
(@eq ?A ?x ?x) =<= (let X : forall _ : nat, nat := ?n in @eq nat (X x) O) (Let-ZetaR)
_(@eq ?A ?x ?x) =<= (@eq nat (?n x) O) (App-FO)
__@eq =<= @eq (Rigid-Same)
__?A =?= nat (Meta-Inst)
___Set =<= Type (Reduce-Same)
__(?n x) =?= ?x (Meta-Inst)
__?x =?= (?n x) (Meta-Inst)
___nat =<= nat (Reduce-Same)
__(?n x) =?= O (Meta-Inst)
___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(@eq nat (let X : forall _ : nat, nat := ?n in X x)
(let X : forall _ : nat, nat := ?n in X x)) =<= (@eq nat O O) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(let X : forall _ : nat, nat := ?n in X x) =?= O (App-FO)
_(let X : forall _ : nat, nat := ?n in X x) =?= O (Let-ZetaL) ERR
(?x = ?x) =<= ((?n : nat -> nat) 0 = 1) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_(?n 0) =?= 1 (Meta-FO) OK
__?n =?= S (Meta-Inst) OK
___(nat -> nat) =<= (nat -> nat) (Reduce-Same) OK
__0 =?= 0 (Reduce-Same)
__(?n x) =?= O (Meta-Inst)
___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
_(let X : forall _ : nat, nat := fun _ : nat => O in X x) =?= O (Reduce-Same)tt
: unit
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq nat ((fun w : forall _ : nat, nat => w) ?w x) O) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
_?x =?= ((fun w : forall _ : nat, nat => w) ?w x) (Meta-Inst)
__nat =<= nat (Reduce-Same)
_(?w x) =?= O (Meta-Inst)
__(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same) OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?T@\{x:=x; x0:=x\} =<= ?A (Meta-Inst)
_?A =<= ?T@\{x:=x; x0:=x\} (Meta-Inst)
(@eq ?T@\{x:=x; x0:=x\} ((fun w : forall x0 : nat, ?T => w) ?w x)
((fun w : forall x0 : nat, ?T => w) ?w x)) =<= (@eq nat O O) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?T@\{x:=x; x0:=x\} =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
_((fun w : forall _ : nat, nat => w) ?w x) =?= O (Lam-BetaL)
__(?w x) =?= O (Meta-Inst)
___(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
_((fun w : forall _ : nat, nat => w) (fun _ : nat => O) x) =?= O (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Type =<= Type (Reduce-Same)
?T =<= nat (Meta-DelDeps) OK
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) =<= nat (App-FO)
_?T =<= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq nat match O return nat with
| O => ?n
| S _ => O
end x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same) ERR
(?x = ?x) =<= (match 0 with
| 0 => (?n : nat -> nat) 0
| S _ => 1
end = 1) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= match 0 with
| 0 => (?n : nat -> nat) 0
| S _ => 1
end (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_match 0 with
| 0 => (?n : nat -> nat) 0
| S _ => 1
end =?= 1 (Case-IotaL) OK
__(?n 0) =?= 1 (Meta-FO) OK
___?n =?= S (Meta-Inst) OK
____(nat -> nat) =<= (nat -> nat) (Reduce-Same) OK
___0 =?= 0 (Reduce-Same)
_?x =?= match O return nat with
| O => ?n
| S _ => O
end (Meta-Inst)
__nat =<= nat (Reduce-Same)
_match O return nat with
| O => ?n
| S _ => O
end =?= x (App-FO)
_match O return nat with
| O => ?n
| S _ => O
end =?= x (Case-IotaL)
__?n =?= x (Meta-Inst)
___nat =<= nat (Reduce-Same) OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Type =<= Type (Reduce-Same)
?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-DelDeps)
_?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-Inst) OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same)
__Type =<= Type (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same) OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same)
nat =<= nat (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq nat
(match O return (forall _ : nat, nat) with
| O => ?n
| S _ => fun _ : nat => O
end x) x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= nat (Meta-Inst)
__Set =<= Type (Reduce-Same)
_?x =?= (match O return (forall _ : nat, nat) with
| O => ?n
| S _ => fun _ : nat => O
end x) (Meta-Inst)
__nat =<= nat (Reduce-Same)
_(match O return (forall _ : nat, nat) with
| O => ?n
| S _ => fun _ : nat => O
end x) =?= x (Case-IotaL)
__(?n x) =?= x (Meta-Inst)
__(?n x) =?= x (Meta-DelDeps)
___(?n x) =?= x (Meta-Inst)
____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Decimal.uint =<= Decimal.uint (Reduce-Same)
Number.uint =<= Number.uint (Reduce-Same)
Type =<= Type (Reduce-Same)
?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-DelDeps)
_?T0 =<= (forall _ : ?T@\{n:=_ANONYMOUS_REL_1\}, nat) (Meta-Inst)
__Type =<= Type (Reduce-Same)
?T =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(@eq nat
(match O return (forall _ : nat, nat) with
| O => ?n
| S _ => fun _ : nat => O
end x)
(match O return (forall _ : nat, nat) with
| O => ?n
| S _ => fun _ : nat => O
end x)) =<= (@eq nat x x) (App-FO)
_@eq =<= @eq (Rigid-Same)
_nat =?= nat (Reduce-Same)
_(match O return (forall _ : nat, nat) with
| O => ?n
| S _ => fun _ : nat => O
end x) =?= x (Case-IotaL)
__(?n x) =?= x (Meta-Inst)
__(?n x) =?= x (Meta-DelDeps)
___(?n x) =?= x (Meta-Inst)
____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
_(match O return (forall _ : nat, nat) with
| O => fun n : nat => n
| S _ => fun _ : nat => O
end x) =?= x (Reduce-Same) OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
?A0 =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
?B =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
?A =<= (prod nat nat) (Meta-Inst)
_Set =<= Type (Reduce-Same)
nat =<= nat (Reduce-Same)
?A =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same) OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_((fun x : nat => ?n) 0) =?= 0 (Meta-Specialize) OK
__?n =?= 0 (Meta-DelDeps) OK
___?n =?= 0 (Meta-Inst) OK
____nat =<= nat (Reduce-Same)
?B =<= nat (Meta-Inst)
_Set =<= Type (Reduce-Same)
(prod nat nat) =<= (prod nat nat) (Reduce-Same)
(@eq ?A ?x ?x) =<= (let X : forall _ : nat, nat := ?n in
@eq (prod nat nat) (@pair nat nat (X x) (X x)) (@pair nat nat (X x) x)) (Let-ZetaR)
_(@eq ?A ?x ?x) =<= (@eq (prod nat nat) (@pair nat nat (?n x) (?n x)) (@pair nat nat (?n x) x)) (App-FO)
__@eq =<= @eq (Rigid-Same)
__?A =?= (prod nat nat) (Meta-Inst)
___Set =<= Type (Reduce-Same)
__?x =?= (@pair nat nat (?n x) (?n x)) (Meta-Inst)
___(prod nat nat) =<= (prod nat nat) (Reduce-Same)
__(@pair nat nat (?n x) (?n x)) =?= (@pair nat nat (?n x) x) (App-FO)
___@pair =?= @pair (Rigid-Same)
___nat =?= nat (Reduce-Same)
___nat =?= nat (Reduce-Same)
___(?n x) =?= (?n x) (Meta-Same-Same)
____x =?= x (Reduce-Same)
___(?n x) =?= x (Meta-Inst) OK
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
___(?n x) =?= x (Meta-DelDeps)
____(?n x) =?= x (Meta-Inst)
_____(forall _ : nat, nat) =<= (forall _ : nat, nat) (Reduce-Same)
?A0 =<= T (Meta-Inst)
_Type =<= Type (Reduce-Same)
T =<= T (Reduce-Same)
?A =<= Prop (Meta-Inst)
_Type =<= Type (Reduce-Same)
Prop =<= Prop (Reduce-Same)
(@eq ?A0 ?x0 ?x0) =<= (@eq Prop (forall (T : Type) (t : T), @eq T t t)
(forall (T : ?T) (t : ?T0), @eq ?A ?x ?y)) (App-FO)
_@eq =<= @eq (Rigid-Same) OK
(?x = ?x) =<= ((?n : nat -> nat) 0 = 0) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= (?n 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_((fun x : nat => ?n) 0) =?= 0 (Meta-Specialize) OK
__?n =?= 0 (Meta-DelDeps) OK
___?n =?= 0 (Meta-Inst) OK
____nat =<= nat (Reduce-Same)
_?A0 =?= Prop (Meta-Inst)
__Type =<= Type (Reduce-Same)
_?x0 =?= (forall (T : Type) (t : T), @eq T t t) (Meta-Inst)
__Prop =<= Prop (Reduce-Same)
_(forall (T : Type) (t : T), @eq T t t) =?= (forall (T : ?T) (t : ?T0), @eq ?A ?x ?y) (App-FO) OK
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
__(forall (T : Type) (t : T), @eq T t t) =?= (forall (T : ?T) (t : ?T0), @eq ?A ?x ?y) (Prod-Same) OK
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
___?T =?= Type (Meta-Inst)
____Type =<= Type (Reduce-Same) OK
?T@\{x:=x; x0:=x; x1:=x\} =<= ?A (Meta-Inst) ERR
_?A =<= ?T@\{x:=x; x0:=x; x1:=x\} (Meta-Inst)
___(forall t : T, @eq T t t) =?= (forall t : ?T, @eq ?A ?x ?y) (App-FO) OK
?T@\{x:=x; x0:=x; x1:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same)
____(forall t : T, @eq T t t) =?= (forall t : ?T, @eq ?A ?x ?y) (Prod-Same)
_____?T =?= T (Meta-Inst)
______Type =<= Type (Reduce-Same)
_____(@eq T t t) =?= (@eq ?A ?x ?y) (App-FO)
______@eq =?= @eq (Rigid-Same)
______?A =?= T (Meta-Inst)
_______Type =<= Type (Reduce-Same)
______?x =?= t (Meta-Inst)
_______T =<= T (Reduce-Same)
______?t =?= t (Meta-Inst)
_______T =<= T (Reduce-Same) OK
(?x = ?x) =<= (?n x x = S x) (App-FO) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_(?n x x) =?= ?x (Meta-Inst) ERR
_?x =?= (?n x x) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_(?n x x) =?= (S x) (Meta-Inst) ERR
_(?n x x) =?= (S x) (Meta-DelDeps) ERR
__(?n x x) =?= (S x) (Meta-Inst)
prod1 =
@eq_refl Prop (forall (T : Type) (t : T), @eq T t t)
: @eq Prop (forall (T : Type) (t : T), @eq T t t)
(forall (T : Type) (t : T), @eq T t t)
?A =<= Prop (Meta-Inst)
_Type =<= Type (Reduce-Same)
Prop =<= Prop (Reduce-Same)
(@eq ?A ?x ?x) =<= (@eq Prop (forall _ : Prop, True) (forall t : Prop, ?P : Prop)) (App-FO)
_@eq =<= @eq (Rigid-Same)
_?A =?= Prop (Meta-Inst)
__Type =<= Type (Reduce-Same)
_?x =?= (forall _ : Prop, True) (Meta-Inst)
__Prop =<= Prop (Reduce-Same) ERR
(?x = ?x) =<= (?n x x = S x) (App-FO) ERR
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_(?n x x) =?= ?x (Meta-Inst) ERR
_?x =?= (?n x x) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_(?n x x) =?= (S x) (Meta-Inst) ERR
_(?n x x) =?= (S x) (Meta-DelDeps) ERR
__(?n x x) =?= (S x) (Meta-Inst)
_(forall _ : Prop, True) =?= (forall t : Prop, ?P : Prop) (App-FO)
__(forall _ : Prop, True) =?= (forall t : Prop, ?P : Prop) (Prod-Same)
___Prop =?= Prop (Reduce-Same)
___?P =?= True (Meta-Inst)
____Prop =<= Prop (Reduce-Same)
ERR
0 =?= 0 (App-FO) OK
_0 =?= 0 (Rigid-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
0 <?= X
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
0 <?= ?X
nat <?= nat
nat <?= nat
nat <?= nat
0 =<= X (App-FO) ERR
_0 =<= X (Cons-DeltaNotStuckR) OK
__?X =<= 0 (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
X =?= 0
nat <?= nat
nat <?= nat
X =?= 0 (App-FO) ERR
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
0 =?= X
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
0 =?= 0
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
0 =?= X (App-FO) ERR
_0 =?= X (Cons-DeltaNotStuckR) OK
__0 =?= 0 (App-FO) OK
___0 =?= 0 (Rigid-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (1 + 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (S
((fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end) 0 0))
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?n =?= ((fix add (n m : nat) {struct n} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end) 0 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (1 + 0) (Cons-DeltaNotStuckR) OK
_(S ?n) =?= (S
((fix add (n m : nat) \{struct n\} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end) 0 0)) (App-FO) OK
__S =?= S (Rigid-Same) OK
__?n =?= ((fix add (n m : nat) \{struct n\} : nat :=
match n with
| 0 => m
| S p => S (add p m)
end) 0 0) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (0 + (fun x : nat => x) 1)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= 1
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
(nat -> nat) <?= nat
(nat -> nat) =<= nat (App-FO) ERR
nat <?= nat
nat <?= nat
?n =?= 0
nat <?= nat
nat <?= nat
nat <?= nat
(S ?n) =?= (0 + (fun x : nat => x) 1) (Cons-DeltaNotStuckR) OK
_(S ?n) =?= 1 (App-FO) OK
__S =?= S (Rigid-Same) OK
__?n =?= 0 (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(0 + (fun x : nat => x) 1) =?= 1
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
?y =?= 0
nat <?= nat
nat <?= nat
nat <?= ?T
Set <?= Type
?y =?= 0 (Meta-Inst) OK
_?T =<= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?y X) =?= 0
nat <?= nat
nat <?= nat
(nat -> nat) <?= (forall x0 : nat, ?T)
nat =?= nat
nat <?= ?T@{x0:=n}
Set <?= Type
(?y X) =?= 0 (Meta-Inst) OK
_(nat -> nat) =<= (forall x0 : nat, ?T) (App-FO) OK
__(nat -> nat) =<= (forall x0 : nat, ?T) (Prod-Same) OK
___nat =?= nat (Reduce-Same) OK
___?T@\{x0:=n\} =<= nat (Meta-Inst) OK
____Set =<= Type (Reduce-Same) OK
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{X:=X; x0:=X}
Set <?= Type
?T@\{X:=X; x0:=X\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(?y X X) =?= X
(?y X X) =?= X
nat <?= nat
nat <?= nat
(?y X X) =?= 0
nat <?= nat
nat <?= nat
(nat -> nat -> nat) <?= (forall x0 x1 : nat, ?T)
nat =?= nat
(nat -> nat) <?= (forall x1 : nat, ?T@{x0:=n})
nat =?= nat
nat <?= ?T@{x0:=n; x1:=n}
Set <?= Type
(?y X X) =?= X (Meta-Inst) ERR
_(?y X X) =?= X (Meta-DelDeps) ERR
_(?y X X) =?= X (Meta-Reduce) OK
__(?y X X) =?= 0 (Meta-Inst) OK
___(nat -> nat -> nat) =<= (forall x0 x1 : nat, ?T) (App-FO) OK
____(nat -> nat -> nat) =<= (forall x0 x1 : nat, ?T) (Prod-Same) OK
_____nat =?= nat (Reduce-Same) OK
_____(nat -> nat) =<= (forall x1 : nat, ?T@\{x0:=n\}) (App-FO) OK
______(nat -> nat) =<= (forall x1 : nat, ?T@\{x0:=n\}) (Prod-Same) OK
_______nat =?= nat (Reduce-Same) OK
_______?T@\{x0:=n; x1:=n\} =<= nat (Meta-Inst) OK
________Set =<= Type (Reduce-Same) OK
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{x:=x; x0:=x}
Set <?= Type
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(?y x x) =?= ?y0
(?y0 x x) =?= ?y
(?y x x) =?= ?y0 (Meta-Inst) ERR
_(?y0 x x) =?= ?y (Meta-DelDeps) ERR
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{x:=x; x0:=x}
Set <?= Type
?T@\{x:=x; x0:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(?y x x) <?= ?y0
?T@{x:=x; x0:=x; x1:=x} <?= ?T0
?y0 =<= (?y x x) (Meta-Inst) OK
_?T@\{x:=x; x0:=x; x1:=x\} =<= ?T0 (Meta-Inst) ERR
_?T0 =<= ?T@\{x:=x; x0:=x; x1:=x\} (Meta-Inst) OK
True <?= True
nat <?= ?T
Set <?= Type
?T@{x:=x; y:=x} <?= ?A
nat <?= ?T@{x:=x; y:=x}
Set <?= Type
(?x = ?x) <?= ((fun y : nat => ?n) x = x)
?A =?= nat
Set <?= Type
?x =?= ((fun y : nat => ?n) x)
nat <?= nat
?n@{x:=x; y:=x} =?= x
?n@{y:=x} =?= x
nat <?= nat
aggressive_double_var =
fun x : nat => eq_refl
: forall x : nat, (fun y : nat => y) x = x
Arguments aggressive_double_var x%nat_scope
nat <?= ?T
Set <?= Type
nat <?= ?T@{x:=x; z:=x}
Set <?= Type
?T@{x:=x; y:=y; z:=x; x0:=y} <?= ?A
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; z:=x; x0:=y}
Set <?= Type
(?x = ?x) <?= ((fun z : nat => ?n) x y = x + y)
?A =?= nat
Set <?= Type
?x =?= ((fun z : nat => ?n) x y)
nat <?= nat
(?n@{x:=x; z:=x} y) =?= (x + y)
?n@{x:=x; z:=x} =?= (Nat.add x)
?n@{z:=x} =?= (Nat.add x)
(nat -> nat) <?= (nat -> nat)
y =?= y
aggressive_double_var' =
fun x y : nat => eq_refl
: forall x y : nat, (fun z : nat => Nat.add z) x y = x + y
Arguments aggressive_double_var' (x y)%nat_scope
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= ?T
Set <?= Type
nat <?= ?T@{x:=x; u:=x}
Set <?= Type
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; u:=x; v:=0}
nat <?= ?T0@{u:=x}
Set <?= Type
nat <?= nat
nat <?= nat
?T@{x:=x; y:=y; u:=x; v:=0; w:=y} <?= ?A
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; u:=x; v:=0; w:=y}
nat <?= ?T@{u:=x; w:=y}
Set <?= Type
nat <?= nat
nat <?= nat
(?x = ?x) <?= ((fun u v w : nat => ?n) x 0 y = x)
?A =?= nat
Set <?= Type
nat <?= nat
nat <?= nat
?x =?= ((fun u v w : nat => ?n) x 0 y)
nat <?= nat
nat <?= nat
nat <?= nat
?n@{x:=x; y:=y; u:=x; v:=0; w:=y} =?= x
?n@{u:=x; w:=y} =?= x
nat <?= nat
nat <?= nat
nat <?= nat
aggressive_const =
fun x _ _ : nat => eq_refl
: forall x y : nat, nat -> (fun u _ _ : nat => u) x 0 y = x
Arguments aggressive_const (x y z)%nat_scope
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?T@{x:=x; y:=y; u:=0; v:=x; w:=y} <?= ?A
nat <?= nat
nat <?= nat
?A =<= ?T@\{x:=x; y:=y; u:=0; v:=x; w:=y\} (Meta-Inst) OK
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; u:=0; v:=x; w:=y}
nat <?= ?T@{v:=x; w:=y}
Set <?= Type
?T@\{v:=x; w:=y\} =<= nat (Meta-DelDeps) OK
_?T@\{v:=x; w:=y\} =<= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?x = ?x) <?= ((fun u v w : nat => ?n) 0 x y = x)
nat <?= nat
nat <?= nat
?A =?= nat
Set <?= Type
nat <?= nat
nat <?= nat
?x =?= ((fun u v w : nat => ?n) 0 x y)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?n@{x:=x; y:=y; u:=0; v:=x; w:=y} =?= x
?n@{v:=x; w:=y} =?= x
nat <?= nat
(?x = ?x) =<= ((fun u v w : nat => ?n) 0 x y = x) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= ((fun u v w : nat => ?n) 0 x y) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_?n@\{v:=x; w:=y\} =?= x (Meta-DelDeps) OK
__?n@\{v:=x; w:=y\} =?= x (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
nat <?= nat
nat <?= nat
aggressive_const' =
fun x _ _ : nat => eq_refl
: forall x y : nat, nat -> (fun _ v _ : nat => v) 0 x y = x
Arguments aggressive_const' (x y z)%nat_scope
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
nat <?= ?T
Set <?= Type
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{y:=y; u:=y}
Set <?= Type
?T@\{y:=y; u:=y\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= ?T@{x:=x; y:=y; u:=y; v:=x}
Set <?= Type
?T@\{x:=x; y:=y; u:=y; v:=x\} =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
?T@{x:=x; y:=y; u:=y; v:=x; w:=0} <?= ?A
nat <?= nat
nat <?= nat
?A =<= ?T@\{x:=x; y:=y; u:=y; v:=x; w:=0\} (Meta-Inst) OK
nat <?= nat
nat <?= nat
nat <?= ?T@{x:=x; y:=y; u:=y; v:=x; w:=0}
nat <?= ?T@{u:=y; v:=x}
Set <?= Type
?T@\{u:=y; v:=x\} =<= nat (Meta-DelDeps) OK
_?T@\{u:=y; v:=x\} =<= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?x = ?x) <?= ((fun u v w : nat => ?n) y x 0 = x)
nat <?= nat
nat <?= nat
?A =?= nat
Set <?= Type
nat <?= nat
nat <?= nat
?x =?= ((fun u v w : nat => ?n) y x 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
?n@{x:=x; y:=y; u:=y; v:=x; w:=0} =?= x
?n@{u:=y; v:=x} =?= x
nat <?= nat
(?x = ?x) =<= ((fun u v w : nat => ?n) y x 0 = x) (App-FO) OK
_@eq =<= @eq (Rigid-Same) OK
_?A =?= nat (Meta-Inst) OK
__Set =<= Type (Reduce-Same) OK
_?x =?= ((fun u v w : nat => ?n) y x 0) (Meta-Inst) OK
__nat =<= nat (Reduce-Same) OK
_?n@\{u:=y; v:=x\} =?= x (Meta-DelDeps) OK
__?n@\{u:=y; v:=x\} =?= x (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
nat <?= nat
nat <?= nat
aggressive_const'' =
fun x _ _ : nat => eq_refl
: forall x y : nat, nat -> (fun _ v _ : nat => v) y x 0 = x
Arguments aggressive_const'' (x y z)%nat_scope
Type <?= Type
?T <?= Type
Type <?= Type
?T =<= Type (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
B <?= B
B <?= B
B <?= ?A
Type <?= Type
?A =<= B (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
B <?= B
Prop <?= Prop
(B -> Prop) <?= (B -> Prop)
(B -> B -> Prop) <?= (B -> B -> Prop)
Prop <?= Prop
((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop) <?= ((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop)
?T0 <?= ?A
?A =<= ?T0 (Meta-Inst) OK
?T1 <?= ?T0
?T1 =<= ?T0 (Meta-Inst) OK
?T <?= A
Type <?= Type
?T =<= A (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
B <?= ?T
Type <?= Type
?T =<= B (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
A <?= A
B <?= ?T@{x:=f1 x1}
B <?= ?T0
Type <?= Type
?T0 =<= B (Meta-DelDeps) OK
_?T0 =<= B (Meta-Inst) OK
__Type =<= Type (Reduce-Same) OK
?T@{x:=f1 x1; x0:=f2 x2} <?= Prop
?T <?= Prop
Type <?= Type
?T =<= Prop (Meta-DelDeps) OK
_?T =<= Prop (Meta-Inst) OK
__Type =<= Type (Reduce-Same) OK
nat <?= nat
?T <?= Type
Type <?= Type
?T =<= Type (Meta-Inst) OK
_Type =<= Type (Reduce-Same) OK
Type <?= Type
(B -> B -> Prop) <?= (B -> B -> Prop)
((A -> B) -> (A -> B) -> Prop) <?= (?B -> ?B -> Prop)
(A -> B) =?= ?B
Type <?= Type
((A -> B) -> Prop) <?= ((A -> B) -> Prop)
((A -> B) -> (A -> B) -> Prop) =<= (?B -> ?B -> Prop) (App-FO) OK
_((A -> B) -> (A -> B) -> Prop) =<= (?B -> ?B -> Prop) (Prod-Same) OK
__?B =?= (A -> B) (Meta-Inst) OK
___Type =<= Type (Reduce-Same) OK
__((A -> B) -> Prop) =<= ((A -> B) -> Prop) (Reduce-Same) OK
Prop <?= Prop
((B -> B -> Prop) -> Prop) <?= ((B -> B -> Prop) -> Prop)
(forall B : Type, (B -> B -> Prop) -> Prop) <?= (forall B : Type, (B -> B -> Prop) -> Prop)
Prop <?= Prop
((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop) <?= ((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop)
((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop) <?= ((forall B : Type, (B -> B -> Prop) -> Prop) -> Prop)
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
(fun x y z : nat => ?n) x y z = y)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = y)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= y
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
(fun x y z : nat => ?n) x y z = y) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = y) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= y (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
(forall z : nat,
(fun _ y _ : nat => y) x y z = (fun _ y _ : nat => y) y y x /\
(fun _ y _ : nat => y) x y z = y) <?= (forall z : nat,
(fun _ y _ : nat => y) x y z = (fun _ y _ : nat => y) y y x /\
(fun _ y _ : nat => y) x y z = y)
(forall y z : nat,
(fun _ y0 _ : nat => y0) x y z = (fun _ y0 _ : nat => y0) y y x /\
(fun _ y0 _ : nat => y0) x y z = y) <?= (forall y z : nat,
(fun _ y0 _ : nat => y0) x y z = (fun _ y0 _ : nat => y0) y y x /\
(fun _ y0 _ : nat => y0) x y z = y)
(forall x y z : nat,
(fun _ y0 _ : nat => y0) x y z = (fun _ y0 _ : nat => y0) y y x /\
(fun _ y0 _ : nat => y0) x y z = y) <?= (let T := fun _ y _ : nat => y in
forall x y z : nat, T x y z = T y y x /\ T x y z = y)
Decimal.uint <?= Decimal.uint
Decimal.uint <?= Decimal.uint
Number.uint <?= Number.uint
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
nat <?= nat
nat <?= nat
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y /\
(fun x y z : nat => ?n) x y z = 0)
nat <?= nat
nat <?= nat
(?x = ?x) =?= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x x x)
nat <?= nat
?n@{x:=x; y:=x; z:=x} =?= ((fun x y z : nat => ?n) y y y)
?n@{z:=x} =?= ((fun _ _ z : nat => ?n) y y y)
?n@{z:=x} =?= ?n@{z:=y}
nat <?= nat
nat <?= nat
(?x = ?x) =?= ((fun _ _ _ : nat => ?n) x y z = 0)
nat <?= nat
nat <?= nat
?A =?= nat
Set <?= Type
?x =?= ((fun _ _ _ : nat => ?n) x y z)
nat <?= nat
nat <?= nat
nat <?= nat
?n =?= 0
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y /\\
(fun x y z : nat => ?n) x y z = 0) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x x x = (fun x y z : nat => ?n) y y y) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x x x) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n@\{x:=x; y:=x; z:=x\} =?= ((fun x y z : nat => ?n) y y y) (Meta-Inst) ERR
__?n@\{z:=x\} =?= ((fun _ _ z : nat => ?n) y y y) (Meta-DelDeps) OK
___?n@\{z:=x\} =?= ((fun _ _ z : nat => ?n) y y y) (Meta-Inst) ERR
___?n@\{z:=x\} =?= ((fun _ _ z : nat => ?n) y y y) (Meta-Reduce) OK
____?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ _ _ : nat => ?n) x y z = 0) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ _ _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= 0 (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(forall z : nat,
(fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
(fun _ _ _ : nat => 0) x y z = 0) <?= (forall z : nat,
(fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
(fun _ _ _ : nat => 0) x y z = 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(forall y z : nat,
(fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
(fun _ _ _ : nat => 0) x y z = 0) <?= (forall y z : nat,
(fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
(fun _ _ _ : nat => 0) x y z = 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(forall x y z : nat,
(fun _ _ _ : nat => 0) x x x = (fun _ _ _ : nat => 0) y y y /\
(fun _ _ _ : nat => 0) x y z = 0) <?= (let T := fun _ _ _ : nat => 0 in
forall x y z : nat, T x x x = T y y y /\ T x y z = 0)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
(fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
(fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
(fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
(fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
(fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
(fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\
(fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) y y x)
?n =?= ?n@{x:=y; y:=y; z:=x}
(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun _ y _ : nat => ?n) x y z)
nat <?= nat
?n =?= x
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x /\\
(fun x y z : nat => ?n) x y z = x) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) y y x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) y y x) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ y _ : nat => ?n) x y z = x) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ y _ : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) ERR
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\
(fun x y z : nat => ?n) x y z = x)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) x z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = x)
?A =?= nat
Set <?= Type
?x =?= ((fun x _ z : nat => ?n) x y z)
nat <?= nat
?n =?= x
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\\
(fun x y z : nat => ?n) x y z = x) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = x) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= x (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
(forall z : nat,
(fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
(fun x _ _ : nat => x) x y z = x) <?= (forall z : nat,
(fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
(fun x _ _ : nat => x) x y z = x)
(forall y z : nat,
(fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
(fun x _ _ : nat => x) x y z = x) <?= (forall y z : nat,
(fun x _ _ : nat => x) x y z = (fun x _ _ : nat => x) x z z /\
(fun x _ _ : nat => x) x y z = x)
(forall x y z : nat,
(fun x0 _ _ : nat => x0) x y z = (fun x0 _ _ : nat => x0) x z z /\
(fun x0 _ _ : nat => x0) x y z = x) <?= (let T := fun x _ _ : nat => x in
forall x y z : nat, T x y z = T x z z /\ T x y z = x)
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z /\
(fun x y z : nat => ?n) x y z = z)
(?x = ?x) =?= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) z y z)
nat <?= nat
?n@{x:=z; z:=z} =?= ((fun x y z : nat => ?n) z z z)
?n =?= ((fun _ y z : nat => ?n) z z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun _ _ z : nat => ?n) x y z = z)
?A =?= nat
Set <?= Type
?x =?= ((fun _ _ z : nat => ?n) x y z)
nat <?= nat
?n =?= z
nat <?= nat
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z /\\
(fun x y z : nat => ?n) x y z = z) (App-FO) OK
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) z y z = (fun x y z : nat => ?n) z z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) z y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n@\{x:=z; z:=z\} =?= ((fun x y z : nat => ?n) z z z) (Meta-Inst) ERR
__?n =?= ((fun _ y z : nat => ?n) z z z) (Meta-DelDeps) OK
___?n =?= ((fun _ y z : nat => ?n) z z z) (Meta-Inst) ERR
___?n =?= ((fun _ y z : nat => ?n) z z z) (Meta-Reduce) OK
____?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun _ _ z : nat => ?n) x y z = z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun _ _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= z (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
(forall z : nat,
(fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
(fun _ _ z0 : nat => z0) x y z = z) <?= (forall z : nat,
(fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
(fun _ _ z0 : nat => z0) x y z = z)
(forall y z : nat,
(fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
(fun _ _ z0 : nat => z0) x y z = z) <?= (forall y z : nat,
(fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
(fun _ _ z0 : nat => z0) x y z = z)
(forall x y z : nat,
(fun _ _ z0 : nat => z0) z y z = (fun _ _ z0 : nat => z0) z z z /\
(fun _ _ z0 : nat => z0) x y z = z) <?= (let T := fun _ _ z : nat => z in
forall x y z : nat, T z y z = T z z z /\ T x y z = z)
(nat -> nat) <?= (nat -> nat)
(nat -> nat -> nat) <?= (nat -> nat -> nat)
(nat -> nat -> nat -> nat) <?= (nat -> nat -> nat -> nat)
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
nat <?= ?A
Set <?= Type
?A =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
nat <?= nat
Prop <?= Prop
nat <?= nat
nat <?= nat
nat <?= nat
(?x = ?x) <?= ?A
Prop <?= Prop
?A =<= (?x = ?x) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x0 = ?x0) <?= ?B
Prop <?= Prop
?B =<= (?x0 = ?x0) (Meta-Inst) OK
_Prop =<= Prop (Reduce-Same) OK
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\
(fun x y z : nat => ?n) x y z = y)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) x z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y)
?A =?= nat
Set <?= Type
?x =?= ((fun x _ z : nat => ?n) x y z)
nat <?= nat
?n =?= y
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\\
(fun x y z : nat => ?n) x y z = y) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= y (Meta-Inst) ERR
(?x = ?x /\ ?x0 = ?x0) <?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\
(fun x y z : nat => ?n) x y z = y)
(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z)
?A =?= nat
Set <?= Type
?x =?= ((fun x y z : nat => ?n) x y z)
nat <?= nat
?n =?= ((fun x y z : nat => ?n) x z z)
?n =?= ?n@{y:=z; z:=z}
(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y)
?A =?= nat
Set <?= Type
?x =?= ((fun x _ z : nat => ?n) x y z)
nat <?= nat
?n =?= y
(?x = ?x /\\ ?x0 = ?x0) =<= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z /\\
(fun x y z : nat => ?n) x y z = y) (App-FO) ERR
_and =<= and (Rigid-Same) OK
_(?x = ?x) =?= ((fun x y z : nat => ?n) x y z = (fun x y z : nat => ?n) x z z) (App-FO) OK
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x y z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Inst) ERR
__?n =?= ((fun x y z : nat => ?n) x z z) (Meta-Reduce) OK
___?n =?= ?n (Meta-Same) OK
_(?x = ?x) =?= ((fun x _ z : nat => ?n) x y z = y) (App-FO) ERR
__@eq =?= @eq (Rigid-Same) OK
__?A =?= nat (Meta-Inst) OK
___Set =<= Type (Reduce-Same) OK
__?x =?= ((fun x _ z : nat => ?n) x y z) (Meta-Inst) OK
___nat =<= nat (Reduce-Same) OK
__?n =?= y (Meta-Inst) ERR
STATS: 902 165
Finished transaction in 2.209 secs (2.149u,0.059s) (successful)
make[1]: Leaving directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
dh_auto_test
create-stamp debian/debhelper-build-stamp
dh_prep
debian/rules override_dh_auto_install
make[1]: Entering directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
DESTDIR=debian/tmp make install
make[2]: Entering directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
INSTALL theories/Unicoq.vo debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/Unicoq/
SKIP test-suite/munifytest.vo since it has no logical path
SKIP test-suite/microtests.vo since it has no logical path
SKIP test-suite/primitive.vo since it has no logical path
SKIP test-suite/instantiate.vo since it has no logical path
SKIP test-suite/timings.vo since it has no logical path
SKIP test-suite/bug_41.vo since it has no logical path
SKIP test-suite/bug_44.vo since it has no logical path
INSTALL theories/Unicoq.v debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/Unicoq/
SKIP test-suite/munifytest.v since it has no logical path
SKIP test-suite/microtests.v since it has no logical path
SKIP test-suite/primitive.v since it has no logical path
SKIP test-suite/instantiate.v since it has no logical path
SKIP test-suite/timings.v since it has no logical path
SKIP test-suite/bug_41.v since it has no logical path
SKIP test-suite/bug_44.v since it has no logical path
INSTALL theories/Unicoq.glob debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/Unicoq/
SKIP test-suite/munifytest.glob since it has no logical path
SKIP test-suite/microtests.glob since it has no logical path
SKIP test-suite/primitive.glob since it has no logical path
SKIP test-suite/instantiate.glob since it has no logical path
SKIP test-suite/timings.glob since it has no logical path
SKIP test-suite/bug_41.glob since it has no logical path
SKIP test-suite/bug_44.glob since it has no logical path
INSTALL src/unicoq.cmxs debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/Unicoq/
INSTALL src/unicoq.cmxs debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq//user-contrib/Unicoq/
ocamlfind: [WARNING] No such file: debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/META
Installed debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/unicoq.cmx
Installed debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/unicoq.cmxa
Installed debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/unicoq.cmxs
ocamlfind: [WARNING] Overwriting file debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/unicoq.cmxs
Installed debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/unicoq.cmxs
Installed debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/unicoq.cmi
Installed debian/tmp//usr/lib/x86_64-linux-gnu/ocaml/5.3.0/coq/../coq-core//../coq-unicoq/META
make[3]: Entering directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
make[3]: Leaving directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
make[2]: Leaving directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
make[1]: Leaving directory '/build/reproducible-path/coq-unicoq-1.6-8.20'
dh_install
dh_ocamldoc
dh_installdocs
dh_installchangelogs
dh_lintian
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
dpkg-gencontrol: warning: package libcoq-unicoq: substitution variable ${ocaml:Depends} unused, but is defined
dpkg-gencontrol: warning: package libcoq-unicoq: substitution variable ${ocaml:Depends} unused, but is defined
dh_md5sums
dh_builddeb
dpkg-deb: building package 'libcoq-unicoq' in '../libcoq-unicoq_1.6-8.20-1_amd64.deb'.
dpkg-deb: building package 'libcoq-unicoq-dbgsym' in '../libcoq-unicoq-dbgsym_1.6-8.20-1_amd64.deb'.
dpkg-genbuildinfo --build=binary -O../coq-unicoq_1.6-8.20-1_amd64.buildinfo
dpkg-genchanges --build=binary -O../coq-unicoq_1.6-8.20-1_amd64.changes
dpkg-genchanges: info: binary-only upload (no source code included)
dpkg-source --after-build .
dpkg-buildpackage: info: binary-only upload (no source included)
dpkg-genchanges: info: including full source code in upload
I: copying local configuration
I: unmounting dev/ptmx filesystem
I: unmounting dev/pts filesystem
I: unmounting dev/shm filesystem
I: unmounting proc filesystem
I: unmounting sys filesystem
I: cleaning the build env
I: removing directory /srv/workspace/pbuilder/2185331 and its subdirectories
I: Current time: Mon Apr 6 05:52:58 -12 2026
I: pbuilder-time-stamp: 1775497978
Tue Mar 4 11:29:59 UTC 2025 I: 1st build successful. Starting 2nd build on remote node ionos1-amd64.debian.net.
Tue Mar 4 11:29:59 UTC 2025 I: Preparing to do remote build '2' on ionos1-amd64.debian.net.
Tue Mar 4 11:34:41 UTC 2025 I: Deleting $TMPDIR on ionos1-amd64.debian.net.
Tue Mar 4 11:34:42 UTC 2025 I: coq-unicoq_1.6-8.20-1_amd64.changes:
Format: 1.8
Date: Sat, 23 Nov 2024 16:03:33 +0100
Source: coq-unicoq
Binary: libcoq-unicoq libcoq-unicoq-dbgsym
Architecture: amd64
Version: 1.6-8.20-1
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Julien Puydt <jpuydt@debian.org>
Description:
libcoq-unicoq - enhanced unification algorithm for Coq
Changes:
coq-unicoq (1.6-8.20-1) unstable; urgency=medium
.
* New upstream release.
Checksums-Sha1:
4e12ad1081c96a9e325722f1a95638116c507325 6136 coq-unicoq_1.6-8.20-1_amd64.buildinfo
d1c4f5b6a87f1dbbfb104578b137ab863ea0b249 23696 libcoq-unicoq-dbgsym_1.6-8.20-1_amd64.deb
91f0f7ec7135004d2ecb803f606d61e97790e7fd 86460 libcoq-unicoq_1.6-8.20-1_amd64.deb
Checksums-Sha256:
e2976498e049daf335d05a66bc656a48cd86c937a285676246dd82321fa01d2f 6136 coq-unicoq_1.6-8.20-1_amd64.buildinfo
9c8f0dd7e25b8eb655fa86e86f7394b60ad0ac3652450544a568ffbba4b489ec 23696 libcoq-unicoq-dbgsym_1.6-8.20-1_amd64.deb
b176bf4727b9ee66e5f558d0404abb772d068d333ffc41fdca3cabdd4dbf7d09 86460 libcoq-unicoq_1.6-8.20-1_amd64.deb
Files:
b0786d7dbf50d38e236b0064b078bed2 6136 ocaml optional coq-unicoq_1.6-8.20-1_amd64.buildinfo
3e4d6e372d42ee1794c8b9ce831a640c 23696 debug optional libcoq-unicoq-dbgsym_1.6-8.20-1_amd64.deb
81cb2c45ddc35c02eee43f815bcadb97 86460 ocaml optional libcoq-unicoq_1.6-8.20-1_amd64.deb
Tue Mar 4 11:34:43 UTC 2025 I: diffoscope 289 will be used to compare the two builds:
Running as unit: rb-diffoscope-amd64_26-33427.service
# Profiling output for: /usr/bin/diffoscope --timeout 7200 --html /srv/reproducible-results/rbuild-debian/r-b-build.3xwkdLWH/coq-unicoq_1.6-8.20-1.diffoscope.html --text /srv/reproducible-results/rbuild-debian/r-b-build.3xwkdLWH/coq-unicoq_1.6-8.20-1.diffoscope.txt --json /srv/reproducible-results/rbuild-debian/r-b-build.3xwkdLWH/coq-unicoq_1.6-8.20-1.diffoscope.json --profile=- /srv/reproducible-results/rbuild-debian/r-b-build.3xwkdLWH/b1/coq-unicoq_1.6-8.20-1_amd64.changes /srv/reproducible-results/rbuild-debian/r-b-build.3xwkdLWH/b2/coq-unicoq_1.6-8.20-1_amd64.changes
## command (total time: 0.000s)
0.000s 1 call cmp (internal)
## has_same_content_as (total time: 0.000s)
0.000s 1 call diffoscope.comparators.binary.FilesystemFile
## main (total time: 0.004s)
0.004s 2 calls outputs
0.000s 1 call cleanup
Finished with result: success
Main processes terminated with: code=exited/status=0
Service runtime: 221ms
CPU time consumed: 222ms
Tue Mar 4 11:34:44 UTC 2025 I: diffoscope 289 found no differences in the changes files, and a .buildinfo file also exists.
Tue Mar 4 11:34:44 UTC 2025 I: coq-unicoq from unstable built successfully and reproducibly on amd64.
Tue Mar 4 11:34:45 UTC 2025 I: Submitting .buildinfo files to external archives:
Tue Mar 4 11:34:45 UTC 2025 I: Submitting 8.0K b1/coq-unicoq_1.6-8.20-1_amd64.buildinfo.asc
Tue Mar 4 11:34:46 UTC 2025 I: Submitting 8.0K b2/coq-unicoq_1.6-8.20-1_amd64.buildinfo.asc
Tue Mar 4 11:34:47 UTC 2025 I: Done submitting .buildinfo files to http://buildinfo.debian.net/api/submit.
Tue Mar 4 11:34:47 UTC 2025 I: Done submitting .buildinfo files.
Tue Mar 4 11:34:47 UTC 2025 I: Removing signed coq-unicoq_1.6-8.20-1_amd64.buildinfo.asc files:
removed './b1/coq-unicoq_1.6-8.20-1_amd64.buildinfo.asc'
removed './b2/coq-unicoq_1.6-8.20-1_amd64.buildinfo.asc'