Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/a/aac-tactics/aac-tactics_8.15.1-2_amd64.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/aac-tactics-8.15.1-2h_x07u3j/aac-tactics_8.15.1-2_amd64.buildinfo Get source package info: aac-tactics=8.15.1-2 Source URL: http://snapshot.notset.fr/mr/package/aac-tactics/8.15.1-2/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.71-2 automake=1:1.16.5-1.3 autopoint=0.21-6 autotools-dev=20220109.1 base-files=12.2 base-passwd=3.5.52 bash=5.1-6 binutils=2.38-3 binutils-common=2.38-3 binutils-x86-64-linux-gnu=2.38-3 bsdextrautils=2.38-2 bsdutils=1:2.37.3-1+b1 build-essential=12.9 bzip2=1.0.8-5 coq=8.15.1+dfsg-1 coreutils=8.32-4.1 cpp=4:11.2.0-2 cpp-11=11.2.0-19 dash=0.5.11+git20210903+057cd650a4ed-8 debconf=1.5.79 debhelper=13.6 debianutils=5.7-0.1 dh-autoreconf=20 dh-ocaml=1.1.3 dh-strip-nondeterminism=1.13.0-1 diffutils=1:3.7-5 dpkg=1.21.7 dpkg-dev=1.21.7 dwz=0.14-1 file=1:5.41-3 findutils=4.9.0-2 g++=4:11.2.0-2 g++-11=11.2.0-19 gcc=4:11.2.0-2 gcc-11=11.2.0-19 gcc-11-base=11.2.0-19 gcc-12-base=12-20220319-1 gettext=0.21-6 gettext-base=0.21-6 grep=3.7-1 groff-base=1.22.4-8 gzip=1.12-1 hostname=3.23 init-system-helpers=1.62 intltool-debian=0.35.0+20060710.5 libacl1=2.3.1-1 libarchive-zip-perl=1.68-1 libasan6=11.2.0-19 libatomic1=12-20220319-1 libattr1=1:2.5.1-1 libaudit-common=1:3.0.7-1 libaudit1=1:3.0.7-1+b1 libbinutils=2.38-3 libblkid1=2.37.3-1+b1 libbz2-1.0=1.0.8-5 libc-bin=2.33-7 libc-dev-bin=2.33-7 libc6=2.33-7 libc6-dev=2.33-7 libcap-ng0=0.7.9-2.2+b2 libcap2=1:2.44-1 libcc1-0=12-20220319-1 libcom-err2=1.46.5-2 libcoq-core-ocaml=8.15.1+dfsg-1 libcoq-core-ocaml-dev=8.15.1+dfsg-1 libcoq-stdlib=8.15.1+dfsg-1 libcrypt-dev=1:4.4.27-1.1 libcrypt1=1:4.4.27-1.1 libctf-nobfd0=2.38-3 libctf0=2.38-3 libdb5.3=5.3.28+dfsg1-0.8 libdebconfclient0=0.261 libdebhelper-perl=13.6 libdpkg-perl=1.21.7 libelf1=0.186-1 libexpat1=2.4.8-1 libffi8=3.4.2-4 libfile-stripnondeterminism-perl=1.13.0-1 libfindlib-ocaml=1.9.3-1 libgcc-11-dev=11.2.0-19 libgcc-s1=12-20220319-1 libgcrypt20=1.10.1-2 libgdbm-compat4=1.23-1 libgdbm6=1.23-1 libgmp-dev=2:6.2.1+dfsg-3 libgmp10=2:6.2.1+dfsg-3 libgmp3-dev=2:6.2.1+dfsg-3 libgmpxx4ldbl=2:6.2.1+dfsg-3 libgomp1=12-20220319-1 libgpg-error0=1.43-3 libgssapi-krb5-2=1.19.2-2+b1 libicu67=67.1-7 libisl23=0.24-2 libitm1=12-20220319-1 libk5crypto3=1.19.2-2+b1 libkeyutils1=1.6.1-3 libkrb5-3=1.19.2-2+b1 libkrb5support0=1.19.2-2+b1 liblsan0=12-20220319-1 liblz4-1=1.9.3-2 liblzma5=5.2.5-2.1 libmagic-mgc=1:5.41-3 libmagic1=1:5.41-3 libmount1=2.37.3-1+b1 libmpc3=1.2.1-2 libmpdec3=2.5.1-2 libmpfr6=4.1.0-3 libncurses-dev=6.3-2 libncurses5-dev=6.3-2 libncurses6=6.3-2 libncursesw6=6.3-2 libnsl-dev=1.3.0-2 libnsl2=1.3.0-2 libpam-modules=1.4.0-11 libpam-modules-bin=1.4.0-11 libpam-runtime=1.4.0-11 libpam0g=1.4.0-11 libpcre2-8-0=10.39-3 libpcre3=2:8.39-14 libperl5.34=5.34.0-4 libpipeline1=1.5.5-1 libpython3-stdlib=3.10.4-1 libpython3.10-minimal=3.10.4-3 libpython3.10-stdlib=3.10.4-3 libquadmath0=12-20220319-1 libreadline8=8.1.2-1 libseccomp2=2.5.3-2 libselinux1=3.3-1+b2 libsigsegv2=2.14-1 libsmartcols1=2.38-2 libsqlite3-0=3.38.2-1 libssl1.1=1.1.1n-1 libstdc++-11-dev=11.2.0-19 libstdc++6=12-20220319-1 libsub-override-perl=0.09-2 libsystemd0=250.4-1 libtinfo6=6.3-2 libtirpc-common=1.3.2-2 libtirpc-dev=1.3.2-2 libtirpc3=1.3.2-2 libtool=2.4.7-3 libtsan0=11.2.0-19 libubsan1=12-20220319-1 libuchardet0=0.0.7-1 libudev1=250.4-1 libunistring2=1.0-1 libuuid1=2.37.3-1+b1 libxml2=2.9.13+dfsg-1 libzarith-ocaml=1.12-1+b1 libzarith-ocaml-dev=1.12-1+b1 libzstd1=1.4.10+dfsg-1 linux-libc-dev=5.16.18-1 login=1:4.11.1+dfsg1-2 lsb-base=11.1.0 m4=1.4.18-5 make=4.3-4.1 man-db=2.10.2-1 mawk=1.3.4.20200120-3+b1 media-types=7.1.0 ncurses-base=6.3-2 ncurses-bin=6.3-2 ocaml=4.13.1-3 ocaml-base=4.13.1-3 ocaml-compiler-libs=4.13.1-3 ocaml-findlib=1.9.3-1 ocaml-interp=4.13.1-3 ocaml-nox=4.13.1-3 patch=2.7.6-7 perl=5.34.0-4 perl-base=5.34.0-4 perl-modules-5.34=5.34.0-4 po-debconf=1.0.21+nmu1 python3=3.10.4-1 python3-minimal=3.10.4-1 python3.10=3.10.4-3 python3.10-minimal=3.10.4-3 readline-common=8.1.2-1 rpcsvc-proto=1.4.2-4 sed=4.8-1 sensible-utils=0.0.17 sysvinit-utils=3.01-1 tar=1.34+dfsg-1 util-linux=2.37.3-1+b1 xz-utils=5.2.5-2.1 zlib1g=1:1.2.11.dfsg-4 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220413T094333Z/ unstable main deb-src http://snapshot.notset.fr/archive/debian/20220413T094333Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220413T211711Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220411T092602Z/ unstable main' >> /etc/apt/sources.list && apt-get update" --customize-hook=chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash --customize-hook=chroot "$1" env sh -c "apt-get source --only-source -d aac-tactics=8.15.1-2 && mkdir -p /build/aac-tactics-zBHIhn && dpkg-source --no-check -x /*.dsc /build/aac-tactics-zBHIhn/aac-tactics-8.15.1 && chown -R builduser:builduser /build/aac-tactics-zBHIhn" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/aac-tactics-zBHIhn/aac-tactics-8.15.1 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1649833668" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any" --customize-hook=sync-out /build/aac-tactics-zBHIhn /tmp/aac-tactics-8.15.1-2h_x07u3j bookworm /dev/null deb http://snapshot.notset.fr/archive/debian/20220411T092602Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: null I: using /tmp/mmdebstrap.G3jiAuMRFn as tempdir I: running apt-get update... I: downloading packages with apt... I: extracting archives... I: installing essential packages... I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "apt-get --yes install fakeroot util-linux"' exec /tmp/mmdebstrap.G3jiAuMRFn Reading package lists... Building dependency tree... util-linux is already the newest version (2.37.3-1+b1). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 135 kB of archives. After this operation, 406 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20220411T092602Z unstable/main amd64 libfakeroot amd64 1.28-1 [48.2 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220411T092602Z unstable/main amd64 fakeroot amd64 1.28-1 [87.2 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 135 kB in 0s (1096 kB/s) Selecting previously unselected package libfakeroot:amd64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 4701 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.28-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.28-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.28-1_amd64.deb ... Unpacking fakeroot (1.28-1) ... Setting up libfakeroot:amd64 (1.28-1) ... Setting up fakeroot (1.28-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.33-7) ... I: running special hook: copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20220413T094333Z/ unstable main deb-src http://snapshot.notset.fr/archive/debian/20220413T094333Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220413T211711Z/ unstable main deb http://snapshot.notset.fr/archive/debian/20220411T092602Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.G3jiAuMRFn Get:1 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable InRelease [165 kB] Get:2 http://snapshot.notset.fr/archive/debian/20220413T211711Z unstable InRelease [165 kB] Hit:3 http://snapshot.notset.fr/archive/debian/20220411T092602Z unstable InRelease Ign:4 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main amd64 Packages Ign:4 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main Sources Ign:5 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main amd64 Packages Get:4 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main Sources [12.9 MB] Get:5 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main amd64 Packages [12.4 MB] Ign:6 http://snapshot.notset.fr/archive/debian/20220413T211711Z unstable/main amd64 Packages Err:6 http://snapshot.notset.fr/archive/debian/20220413T211711Z unstable/main amd64 Packages 404 Not Found [IP: 10.13.0.253 80] Ign:6 http://snapshot.notset.fr/archive/debian/20220413T211711Z unstable/main amd64 Packages Get:6 http://snapshot.notset.fr/archive/debian/20220413T211711Z unstable/main amd64 Packages [12.4 MB] Fetched 38.0 MB in 30s (1245 kB/s) Reading package lists... I: installing remaining packages inside the chroot... I: running --customize-hook in shell: sh -c 'chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash' exec /tmp/mmdebstrap.G3jiAuMRFn I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d aac-tactics=8.15.1-2 && mkdir -p /build/aac-tactics-zBHIhn && dpkg-source --no-check -x /*.dsc /build/aac-tactics-zBHIhn/aac-tactics-8.15.1 && chown -R builduser:builduser /build/aac-tactics-zBHIhn"' exec /tmp/mmdebstrap.G3jiAuMRFn Reading package lists... NOTICE: 'aac-tactics' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/ocaml-team/aac-tactics.git Please use: git clone https://salsa.debian.org/ocaml-team/aac-tactics.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 74.2 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main aac-tactics 8.15.1-2 (dsc) [2209 B] Get:2 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main aac-tactics 8.15.1-2 (tar) [68.3 kB] Get:3 http://snapshot.notset.fr/archive/debian/20220413T094333Z unstable/main aac-tactics 8.15.1-2 (diff) [3720 B] Fetched 74.2 kB in 0s (825 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'aac-tactics_8.15.1-2.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting aac-tactics in /build/aac-tactics-zBHIhn/aac-tactics-8.15.1 dpkg-source: info: unpacking aac-tactics_8.15.1.orig.tar.gz dpkg-source: info: unpacking aac-tactics_8.15.1-2.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/aac-tactics-zBHIhn/aac-tactics-8.15.1 && env DEB_BUILD_OPTIONS="parallel=4" LC_ALL="C.UTF-8" LC_COLLATE="C.UTF-8" SOURCE_DATE_EPOCH="1649833668" DEB_BUILD_OPTIONS=nocheck dpkg-buildpackage -uc -a amd64 --build=any"' exec /tmp/mmdebstrap.G3jiAuMRFn dpkg-buildpackage: info: source package aac-tactics dpkg-buildpackage: info: source version 8.15.1-2 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Julien Puydt dpkg-source --before-build . dpkg-buildpackage: info: host architecture amd64 debian/rules clean dh clean --with ocaml debian/rules override_dh_auto_clean make[1]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' /usr/bin/make clean make[2]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' coq_makefile -f _CoqProject -o Makefile.coq make[3]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' rm -f src/aac.cmo src/coq.cmo src/helper.cmo src/search_monad.cmo src/matcher.cmo src/theory.cmo src/print.cmo src/aac_rewrite.cmo src/aac_plugin.cmo rm -f src/aac.cmi src/coq.cmi src/helper.cmi src/search_monad.cmi src/matcher.cmi src/theory.cmi src/print.cmi src/aac_rewrite.cmi src/aac_plugin.cmi src/coq.cmi src/helper.cmi src/search_monad.cmi src/matcher.cmi src/theory.cmi src/print.cmi src/aac_rewrite.cmi rm -f src/aac_plugin.cma rm -f src/aac.cmx src/coq.cmx src/helper.cmx src/search_monad.cmx src/matcher.cmx src/theory.cmx src/print.cmx src/aac_rewrite.cmx src/aac_plugin.cmx rm -f src/aac_plugin.cmxa rm -f src/aac_plugin.cmxs src/aac_plugin.cmxs rm -f src/aac.o src/coq.o src/helper.o src/search_monad.o src/matcher.o src/theory.o src/print.o src/aac_rewrite.o src/aac_plugin.o rm -f src/aac_plugin.a rm -f src/aac.ml rm -f src/aac.mlg.d src/coq.ml.d src/helper.ml.d src/search_monad.ml.d src/matcher.ml.d src/theory.ml.d src/print.ml.d src/aac_rewrite.ml.d src/aac_plugin.mlpack.d src/coq.mli.d src/helper.mli.d src/search_monad.mli.d src/matcher.mli.d src/theory.mli.d src/print.mli.d src/aac_rewrite.mli.d .Makefile.coq.d rm -f find . -name .coq-native -type d -empty -delete rm -f theories/Utils.vo theories/Constants.vo theories/AAC.vo theories/Instances.vo theories/Tutorial.vo theories/Caveats.vo rm -f theories/Utils.vio theories/Constants.vio theories/AAC.vio theories/Instances.vio theories/Tutorial.vio theories/Caveats.vio rm -f theories/Utils.vos theories/Constants.vos theories/AAC.vos theories/Instances.vos theories/Tutorial.vos theories/Caveats.vos rm -f theories/Utils.vok theories/Constants.vok theories/AAC.vok theories/Instances.vok theories/Tutorial.vok theories/Caveats.vok rm -f theories/Utils.v.beautified theories/Constants.v.beautified theories/AAC.v.beautified theories/Instances.v.beautified theories/Tutorial.v.beautified theories/Caveats.v.beautified theories/Utils.v.old theories/Constants.v.old theories/AAC.v.old theories/Instances.v.old theories/Tutorial.v.old theories/Caveats.v.old rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex rm -f theories/Utils.glob theories/Constants.glob theories/AAC.glob theories/Instances.glob theories/Tutorial.glob theories/Caveats.glob rm -f theories/Utils.tex theories/Constants.tex theories/AAC.tex theories/Instances.tex theories/Tutorial.tex theories/Caveats.tex rm -f theories/Utils.g.tex theories/Constants.g.tex theories/AAC.g.tex theories/Instances.g.tex theories/Tutorial.g.tex theories/Caveats.g.tex rm -f pretty-timed-success.ok rm -rf html mlihtml rm -f theories/.Utils.aux theories/.Constants.aux theories/.AAC.aux theories/.Instances.aux theories/.Tutorial.aux theories/.Caveats.aux rm -f time-of-build.log time-of-build-before.log time-of-build-after.log time-of-build-pretty.log time-of-build-both.log rm -f theories/Utils.v.timing theories/Constants.v.timing theories/AAC.v.timing theories/Instances.v.timing theories/Tutorial.v.timing theories/Caveats.v.timing rm -f theories/Utils.v.before-timing theories/Constants.v.before-timing theories/AAC.v.before-timing theories/Instances.v.before-timing theories/Tutorial.v.before-timing theories/Caveats.v.before-timing rm -f theories/Utils.v.after-timing theories/Constants.v.after-timing theories/AAC.v.after-timing theories/Instances.v.after-timing theories/Tutorial.v.after-timing theories/Caveats.v.after-timing rm -f theories/Utils.v.timing.diff theories/Constants.v.timing.diff theories/AAC.v.timing.diff theories/Instances.v.timing.diff theories/Tutorial.v.timing.diff theories/Caveats.v.timing.diff rm -f .lia.cache .nia.cache make[3]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' make[2]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' make[1]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' dh_ocamlclean dh_clean debian/rules binary-arch dh binary-arch --with ocaml dh_update_autotools_config -a dh_autoreconf -a dh_ocamlinit -a dh_auto_configure -a debian/rules override_dh_auto_build make[1]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' /usr/bin/make Makefile.coq make[2]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' coq_makefile -f _CoqProject -o Makefile.coq make[2]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' /usr/bin/make -f Makefile.coq opt byte html make[2]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' "coqdep" -vos -dyndep var -f _CoqProject > ".Makefile.coq.d" || ( RV=$?; rm -f ".Makefile.coq.d"; exit $RV ) "coqpp" src/aac.mlg "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac_rewrite.mli" > "src/aac_rewrite.mli.d" || ( RV=$?; rm -f "src/aac_rewrite.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/print.mli" > "src/print.mli.d" || ( RV=$?; rm -f "src/print.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/theory.mli" > "src/theory.mli.d" || ( RV=$?; rm -f "src/theory.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/matcher.mli" > "src/matcher.mli.d" || ( RV=$?; rm -f "src/matcher.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/search_monad.mli" > "src/search_monad.mli.d" || ( RV=$?; rm -f "src/search_monad.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/helper.mli" > "src/helper.mli.d" || ( RV=$?; rm -f "src/helper.mli.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/coq.mli" > "src/coq.mli.d" || ( RV=$?; rm -f "src/coq.mli.d"; exit $RV ) "ocamllibdep" -c -I src "src/aac_plugin.mlpack" > "src/aac_plugin.mlpack.d" || ( RV=$?; rm -f "src/aac_plugin.mlpack.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac_rewrite.ml" > "src/aac_rewrite.ml.d" || ( RV=$?; rm -f "src/aac_rewrite.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/print.ml" > "src/print.ml.d" || ( RV=$?; rm -f "src/print.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/theory.ml" > "src/theory.ml.d" || ( RV=$?; rm -f "src/theory.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/matcher.ml" > "src/matcher.ml.d" || ( RV=$?; rm -f "src/matcher.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/search_monad.ml" > "src/search_monad.ml.d" || ( RV=$?; rm -f "src/search_monad.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/helper.ml" > "src/helper.ml.d" || ( RV=$?; rm -f "src/helper.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/coq.ml" > "src/coq.ml.d" || ( RV=$?; rm -f "src/coq.ml.d"; exit $RV ) "/usr/bin/ocamlfind" ocamldep -slash -ml-synonym .mlpack -I src "src/aac.ml" > "src/aac.mlg.d" || ( RV=$?; rm -f "src/aac.mlg.d"; exit $RV ) /usr/bin/make all "OPT:=-opt" -f "Makefile.coq" make[3]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' /usr/bin/make --no-print-directory -f "Makefile.coq" pre-all if [ "8.15.1" != "8.15.1" ]; then\ echo "W: This Makefile was generated by Coq 8.15.1";\ echo "W: while the current Coq version is 8.15.1";\ fi /usr/bin/make --no-print-directory -f "Makefile.coq" real-all "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Utils.v "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Constants.v "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/coq.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/coq.ml "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/helper.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/helper.ml "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/search_monad.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/search_monad.ml "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/matcher.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/matcher.ml File "src/matcher.ml", line 191, characters 26-44: 191 | let nf_term_compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/theory.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/theory.ml File "src/theory.ml", line 892, characters 24-42: 892 | cap t (List.sort (Pervasives.compare) indices) ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/print.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/print.ml File "src/print.ml", line 83, characters 42-60: 83 | let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/aac_rewrite.mli "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/aac_rewrite.ml "/usr/bin/ocamlfind" opt -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -for-pack Aac_plugin src/aac.ml "/usr/bin/ocamlfind" opt -linkpkg -dontlink str,unix,dynlink,threads,zarith -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -pack -o src/aac_plugin.cmx src/coq.cmx src/helper.cmx src/search_monad.cmx src/matcher.cmx src/theory.cmx src/print.cmx src/aac_rewrite.cmx src/aac.cmx "/usr/bin/ocamlfind" opt -linkpkg -dontlink str,unix,dynlink,threads,zarith -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -a -o src/aac_plugin.cmxa src/aac_plugin.cmx "/usr/bin/ocamlfind" opt -linkpkg -dontlink str,unix,dynlink,threads,zarith -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 \ -shared -linkall -o src/aac_plugin.cmxs src/aac_plugin.cmxa "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/AAC.v "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Instances.v "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Tutorial.v All solutions: occurrence 0: transitivity through forall x : X, plus x x 1 possible(s) substitution(s) 0: [x: f (a + a); ] occurrence 1: transitivity through forall x : X, plus (f (x + x)) (f (a + a)) 1 possible(s) substitution(s) 0: [x: a; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 4 possible(s) substitution(s) 0: [x: c; y: dot (d * c * d) b; ] 1: [x: dot c d; y: dot (c * d) b; ] 2: [x: dot (c * d) c; y: dot d b; ] 3: [x: dot (c * d * c) d; y: b; ] occurrence 1: transitivity through forall x y : X, dot (a * x * y * b) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 1 possible(s) substitution(s) 0: [x: plus (c * d) (c * d); y: b; ] All solutions: occurrence 0: transitivity through forall x : X, dot (a * x) a 1 possible(s) substitution(s) 0: [x: 1; ] All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: a; y: c; z: dot b c; ] 1: [x: a; y: dot b c; z: c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * c) 2 possible(s) substitution(s) 0: [x: a; y: dot b c; z: b; ] 1: [x: a; y: b; z: dot b c; ] occurrence 2: transitivity through forall x y z : X, plus (x * y + x * z) (a * b * c) 2 possible(s) substitution(s) 0: [x: a; y: c; z: b; ] 1: [x: a; y: b; z: c; ] File "./theories/Tutorial.v", line 232, characters 6-24: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y) (x * z) 6 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: dot a b; ] 1: [x: a; y: plus (b * c) c; z: b; ] 2: [x: 1; y: 0; z: plus (a * (b * c + c)) (a * b); ] 3: [x: 1; y: plus (a * (b * c + c)) (a * b); z: 0; ] 4: [x: 1; y: dot a b; z: dot a (b * c + c); ] 5: [x: a; y: b; z: plus (b * c) c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: 0; ] 1: [x: 1; y: 0; z: dot a (b * c + c); ] occurrence 2: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * b) 4 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: c; ] 1: [x: 1; y: 0; z: plus (b * c) c; ] 2: [x: 1; y: plus (b * c) c; z: 0; ] 3: [x: 1; y: c; z: dot b c; ] occurrence 3: transitivity through forall x y z : X, plus (a * (x * y + x * z + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: 0; ] 1: [x: 1; y: 0; z: dot b c; ] occurrence 4: transitivity through forall x y z : X, plus (x * y + x * z) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: dot a b; z: 0; ] 1: [x: 1; y: 0; z: dot a b; ] occurrence 5: transitivity through forall x y z : X, plus (a * (b * (x * y + x * z) + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 6: transitivity through forall x y z : X, plus (a * ((x * y + x * z) * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 7: transitivity through forall x y z : X, plus (a * (x * y + x * z + b * c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 8: transitivity through forall x y z : X, plus ((x * y + x * z) * (b * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 9: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 10: transitivity through forall x y z : X, plus ((x * y + x * z) * b) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 11: transitivity through plus (a * (b * c + c)) ((1 * 1 + 1 * 0) * (a * b)) occurrence 12: transitivity through plus (a * (b * c + c)) (a * b * (1 * 1 + 1 * 0)) occurrence 13: transitivity through plus (a * (b * c + c)) (a * ((1 * 1 + 1 * 0) * b)) occurrence 14: transitivity through plus (a * b) ((1 * 1 + 1 * 0) * (a * (b * c + c))) occurrence 15: transitivity through plus (a * b) (a * (b * c + c) * (1 * 1 + 1 * 0)) occurrence 16: transitivity through plus (a * b) (a * (b * c + (1 * 1 + 1 * 0) * c)) occurrence 17: transitivity through plus (a * b) (a * (b * c + c * (1 * 1 + 1 * 0))) occurrence 18: transitivity through plus (a * b) (a * (c + (1 * 1 + 1 * 0) * (b * c))) occurrence 19: transitivity through plus (a * b) (a * (c + b * c * (1 * 1 + 1 * 0))) occurrence 20: transitivity through plus (a * b) (a * (c + b * ((1 * 1 + 1 * 0) * c))) occurrence 21: transitivity through plus (a * b) (a * ((1 * 1 + 1 * 0) * (b * c + c))) occurrence 22: transitivity through dot (a * (b * c + c) + a * b) (1 * 1 + 1 * 0) occurrence 23: transitivity through dot (1 * 1 + 1 * 0) (a * (b * c + c) + a * b) occurrence 24: transitivity through plus (a * (b * c + c)) ((1 * 0 + 1 * 1) * (a * b)) occurrence 25: transitivity through plus (a * (b * c + c)) (a * b * (1 * 0 + 1 * 1)) occurrence 26: transitivity through plus (a * (b * c + c)) (a * ((1 * 0 + 1 * 1) * b)) occurrence 27: transitivity through plus (a * b) ((1 * 0 + 1 * 1) * (a * (b * c + c))) occurrence 28: transitivity through plus (a * b) (a * (b * c + c) * (1 * 0 + 1 * 1)) occurrence 29: transitivity through plus (a * b) (a * (b * c + (1 * 0 + 1 * 1) * c)) occurrence 30: transitivity through plus (a * b) (a * (b * c + c * (1 * 0 + 1 * 1))) occurrence 31: transitivity through plus (a * b) (a * (c + (1 * 0 + 1 * 1) * (b * c))) occurrence 32: transitivity through plus (a * b) (a * (c + b * c * (1 * 0 + 1 * 1))) occurrence 33: transitivity through plus (a * b) (a * (c + b * ((1 * 0 + 1 * 1) * c))) occurrence 34: transitivity through plus (a * b) (a * ((1 * 0 + 1 * 1) * (b * c + c))) occurrence 35: transitivity through dot (a * (b * c + c) + a * b) (1 * 0 + 1 * 1) occurrence 36: transitivity through dot (1 * 0 + 1 * 1) (a * (b * c + c) + a * b) occurrence 37: transitivity through plus (a * (b * c + c) + a * b) (1 * 0 + 1 * 0) occurrence 38: transitivity through plus (a * (b * c + c)) (a * (b + (1 * 0 + 1 * 0))) occurrence 39: transitivity through plus (a * (b * c + c)) ((a + (1 * 0 + 1 * 0)) * b) occurrence 40: transitivity through plus (a * b) (a * (b * c + c + (1 * 0 + 1 * 0))) occurrence 41: transitivity through plus (a * b) (a * (c + b * (c + (1 * 0 + 1 * 0)))) occurrence 42: transitivity through plus (a * b) (a * (c + (b + (1 * 0 + 1 * 0)) * c)) occurrence 43: transitivity through plus (a * b) ((a + (1 * 0 + 1 * 0)) * (b * c + c)) occurrence 44: transitivity through plus (a * (b * c + c) + a * b) (0 * 1 + 0 * 1) occurrence 45: transitivity through plus (a * (b * c + c)) (a * (b + (0 * 1 + 0 * 1))) occurrence 46: transitivity through plus (a * (b * c + c)) ((a + (0 * 1 + 0 * 1)) * b) occurrence 47: transitivity through plus (a * b) (a * (b * c + c + (0 * 1 + 0 * 1))) occurrence 48: transitivity through plus (a * b) (a * (c + b * (c + (0 * 1 + 0 * 1)))) occurrence 49: transitivity through plus (a * b) (a * (c + (b + (0 * 1 + 0 * 1)) * c)) occurrence 50: transitivity through plus (a * b) ((a + (0 * 1 + 0 * 1)) * (b * c + c)) occurrence 51: transitivity through plus (a * (b * c + c)) (a * b * (1 + (1 * 0 + 1 * 0))) occurrence 52: transitivity through plus (a * (b * c + c)) (a * ((1 + (1 * 0 + 1 * 0)) * b)) occurrence 53: transitivity through plus (a * (b * c + c)) ((1 + (1 * 0 + 1 * 0)) * (a * b)) occurrence 54: transitivity through plus (a * b) (a * (b * c + c) * (1 + (1 * 0 + 1 * 0))) occurrence 55: transitivity through plus (a * b) (a * (c + b * c * (1 + (1 * 0 + 1 * 0)))) occurrence 56: transitivity through plus (a * b) (a * (c + b * ((1 + (1 * 0 + 1 * 0)) * c))) occurrence 57: transitivity through plus (a * b) (a * (c + (1 + (1 * 0 + 1 * 0)) * (b * c))) occurrence 58: transitivity through plus (a * b) (a * ((1 + (1 * 0 + 1 * 0)) * (b * c + c))) occurrence 59: transitivity through plus (a * b) ((1 + (1 * 0 + 1 * 0)) * (a * (b * c + c))) occurrence 60: transitivity through plus (a * (b * c + c)) (a * b * (1 + (0 * 1 + 0 * 1))) occurrence 61: transitivity through plus (a * (b * c + c)) (a * ((1 + (0 * 1 + 0 * 1)) * b)) occurrence 62: transitivity through plus (a * (b * c + c)) ((1 + (0 * 1 + 0 * 1)) * (a * b)) occurrence 63: transitivity through plus (a * b) (a * (b * c + c) * (1 + (0 * 1 + 0 * 1))) occurrence 64: transitivity through plus (a * b) (a * (c + b * c * (1 + (0 * 1 + 0 * 1)))) occurrence 65: transitivity through plus (a * b) (a * (c + b * ((1 + (0 * 1 + 0 * 1)) * c))) occurrence 66: transitivity through plus (a * b) (a * (c + (1 + (0 * 1 + 0 * 1)) * (b * c))) occurrence 67: transitivity through plus (a * b) (a * ((1 + (0 * 1 + 0 * 1)) * (b * c + c))) occurrence 68: transitivity through plus (a * b) ((1 + (0 * 1 + 0 * 1)) * (a * (b * c + c))) All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] Discriminated database Unfoldable variable definitions: all Unfoldable constant definitions: all except: CRelationClasses.Antisymmetric Antisymmetric Associative CRelationClasses.Asymmetric Asymmetric Commutative Idempotent CRelationClasses.Irreflexive Irreflexive CMorphisms.Normalizes Normalizes CRelationClasses.PartialOrder PartialOrder CMorphisms.Proper Proper CMorphisms.ProperProxy ProperProxy CRelationClasses.Reflexive Reflexive ssrclasses.Reflexive CRelationClasses.Symmetric Symmetric CRelationClasses.Transitive Transitive Unconvertible all Basics.arrow arrows Basics.compose Basics.const Basics.flip CMorphisms.forall_relation forall_relation id iff Basics.impl not pointwise_lifting CMorphisms.pointwise_relation pointwise_relation predicate_equivalence predicate_implication CRelationClasses.relation_equivalence relation_equivalence CMorphisms.respectful respectful CRelationClasses.subrelation subrelation Cut: emp For any goal -> For Symmetric -> exact iff_Symmetric(level 0, pattern Symmetric iff, id 0) simple apply @eq_Symmetric(level 0, pattern Symmetric eq, id 0) simple apply @Equivalence.equiv_symmetric(level 1, pattern Symmetric Equivalence.equiv, id 0) simple apply @Equivalence_Symmetric(level 1, pattern Symmetric ?META257, id 0) (*external*) (class_apply @flip_Symmetric)(level 3, pattern Symmetric (Basics.flip _), id 0) (*external*) (class_apply @complement_Symmetric)(level 3, pattern Symmetric (complement _), id 0) simple apply @PER_Symmetric(level 3, pattern Symmetric ?META239, id 0) simple apply @Equivalence.pointwise_symmetric(level 9, pattern Symmetric (pointwise_relation ?META411 ?META413), id 0) For Antisymmetric -> simple eapply @partial_order_antisym(level 2, pattern Antisymmetric ?META316 ?META317 ?META319, id 0) (*external*) (class_apply @flip_Antisymmetric)(level 3, pattern Antisymmetric _ (Basics.flip _), id 0) For CMorphisms.Normalizes -> (*external*) CMorphisms.normalizes(level 1, pattern CMorphisms.Normalizes _ _ _, id 0) For CMorphisms.ProperProxy -> (*external*) (class_apply @CMorphisms.eq_proper_proxy || class_apply @CMorphisms.reflexive_proper_proxy)(level 1, pattern CMorphisms.ProperProxy _ _, id 0) (*external*) (not_evar R; class_apply @CMorphisms.proper_proper_proxy)(level 2, pattern CMorphisms.ProperProxy ?R _, id 0) For Unconvertible -> (*external*) unconvertible(level 0, pattern Unconvertible _ _ _, id 0) For Associative -> exact aac_Zmax_Assoc(level 0, pattern Associative eq BinIntDef.Z.max, id 0) exact aac_Zmin_Assoc(level 0, pattern Associative eq BinIntDef.Z.min, id 0) exact aac_Zmult_Assoc(level 0, pattern Associative eq BinIntDef.Z.mul, id 0) exact aac_Zplus_Assoc(level 0, pattern Associative eq BinIntDef.Z.add, id 0) For CRelationClasses.Reflexive -> exact CRelationClasses.iffT_Reflexive(level 0, pattern CRelationClasses.Reflexive CRelationClasses.iffT, id 0) exact CRelationClasses.arrow_Reflexive(level 0, pattern CRelationClasses.Reflexive CRelationClasses.arrow, id 0) exact CRelationClasses.iff_Reflexive(level 0, pattern CRelationClasses.Reflexive iff, id 0) exact CRelationClasses.impl_Reflexive(level 0, pattern CRelationClasses.Reflexive Basics.impl, id 0) simple apply @CRelationClasses.eq_Reflexive(level 0, pattern CRelationClasses.Reflexive eq, id 0) simple apply @CMorphisms.reflexive_eq_dom_reflexive(level 1, pattern CRelationClasses.Reflexive (CMorphisms.respectful eq ?META303), id 0) (*external*) ( class_apply @CRelationClasses.irreflexivity)(level 1, pattern CRelationClasses.Reflexive (CRelationClasses.complement _), id 0) simple apply @CRelationClasses.Equivalence_Reflexive(level 1, pattern CRelationClasses.Reflexive ?META203, id 0) simple apply @CRelationClasses.PreOrder_Reflexive(level 2, pattern CRelationClasses.Reflexive ?META161, id 0) (*external*) ( apply CRelationClasses.flip_Reflexive)(level 3, pattern CRelationClasses.Reflexive (CRelationClasses.flip _), id 0) For ssrclasses.Reflexive -> exact ssrclasses.iff_Reflexive(level 0, pattern ssrclasses.Reflexive iff, id 0) simple apply @ssrclasses.eq_Reflexive(level 0, pattern ssrclasses.Reflexive eq, id 0) simple apply @ssrsetoid.compat_Reflexive(level 12, pattern ssrclasses.Reflexive ?META268, id 0) For Commutative -> exact aac_Zmax_Comm(level 0, pattern Commutative eq BinIntDef.Z.max, id 0) exact aac_Zmin_Comm(level 0, pattern Commutative eq BinIntDef.Z.min, id 0) exact aac_Zmult_Comm(level 0, pattern Commutative eq BinIntDef.Z.mul, id 0) exact aac_Zplus_Comm(level 0, pattern Commutative eq BinIntDef.Z.add, id 0) For Reflexive -> exact iff_Reflexive(level 0, pattern Reflexive iff, id 0) exact impl_Reflexive(level 0, pattern Reflexive Basics.impl, id 0) simple apply @eq_Reflexive(level 0, pattern Reflexive eq, id 0) simple apply @Equivalence.equiv_reflexive(level 1, pattern Reflexive Equivalence.equiv, id 0) simple apply @reflexive_eq_dom_reflexive(level 1, pattern Reflexive (respectful eq ?META358), id 0) (*external*) (class_apply @irreflexivity)(level 1, pattern Reflexive (complement _), id 0) simple apply @Equivalence_Reflexive(level 1, pattern Reflexive ?META251, id 0) simple apply @PreOrder_Reflexive(level 2, pattern Reflexive ?META209, id 0) (*external*) (apply flip_Reflexive)(level 3, pattern Reflexive (Basics.flip _), id 0) exact Z.divide_reflexive(level 5, pattern Reflexive Z.divide, id 0) exact N.divide_reflexive(level 5, pattern Reflexive N.divide, id 0) exact Nat.divide_reflexive(level 5, pattern Reflexive Nat.divide, id 0) simple apply @Equivalence.pointwise_reflexive(level 9, pattern Reflexive (pointwise_relation ?META403 ?META405), id 0) For CRelationClasses.Asymmetric -> simple apply @CRelationClasses.StrictOrder_Asymmetric(level 1, pattern CRelationClasses.Asymmetric ?META185, id 0) (*external*) ( class_apply @CRelationClasses.flip_Asymmetric)(level 3, pattern CRelationClasses.Asymmetric (CRelationClasses.flip _), id 0) For CRelationClasses.Irreflexive -> simple apply @CRelationClasses.StrictOrder_Irreflexive(level 1, pattern CRelationClasses.Irreflexive ?META173, id 0) (*external*) ( class_apply @CRelationClasses.flip_Irreflexive)(level 3, pattern CRelationClasses.Irreflexive (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CRelationClasses.complement_Irreflexive)(level 3, pattern CRelationClasses.Irreflexive (CRelationClasses.complement _), id 0) For Proper -> exact Qminmax.Q.min_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qminmax.Qmin, id 0) exact Qminmax.Q.max_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qminmax.Qmax, id 0) exact Qminmax.Q.Proper_instance_0(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qle, id 0) exact Qminmax.Q.OT.lt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) exact QOrderedType.QOrder.TO.lt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) exact QOrderedType.Q_as_OT.lt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) simple apply FMapPositive.PositiveMap.ME.ltk_compat'(level 0, pattern Proper (FMapPositive.PositiveMap.ME.eqke (elt:=?META923) ==> FMapPositive.PositiveMap.ME.eqke (elt:=?META923) ==> iff) (FMapPositive.PositiveMap.ME.ltk (elt:=?META923)), id 0) simple apply FMapPositive.PositiveMap.ME.ltk_compat(level 0, pattern Proper (FMapPositive.PositiveMap.ME.eqk (elt:=?META921) ==> FMapPositive.PositiveMap.ME.eqk (elt:=?META921) ==> iff) (FMapPositive.PositiveMap.ME.ltk (elt:=?META921)), id 0) exact FMapPositive.PositiveMap.ME.MO.lt_compat(level 0, pattern Proper (eq ==> eq ==> iff) OrderedTypeEx.PositiveOrderedTypeBits.bits_lt, id 0) simple apply SetoidList.rev_eqlistA_compat(level 0, pattern Proper (SetoidList.eqlistA ?META812 ==> SetoidList.eqlistA ?META812) (List.rev (A:=?META811)), id 0) simple apply SetoidList.app_eqlistA_compat(level 0, pattern Proper (SetoidList.eqlistA ?META808 ==> SetoidList.eqlistA ?META808 ==> SetoidList.eqlistA ?META808) (app (A:=?META807)), id 0) simple apply Permutation.Permutation_flat_map(level 0, pattern Proper (Permutation.Permutation (A:=?META1109) ==> Permutation.Permutation (A:=?META1110)) (List.flat_map ?META1111), id 0) simple apply Permutation.Permutation_map'(level 0, pattern Proper (Permutation.Permutation (A:=?META1103) ==> Permutation.Permutation (A:=?META1104)) (List.map ?META1105), id 0) simple apply Permutation.Permutation_NoDup'(level 0, pattern Proper (Permutation.Permutation (A:=?META1101) ==> iff) (List.NoDup (A:=?META1101)), id 0) simple apply Permutation.Permutation_Exists(level 0, pattern Proper (Permutation.Permutation (A:=?META1097) ==> Basics.impl) (List.Exists ?META1098), id 0) simple apply Permutation.Permutation_Forall(level 0, pattern Proper (Permutation.Permutation (A:=?META1093) ==> Basics.impl) (List.Forall ?META1094), id 0) simple apply Permutation.Permutation_rev'(level 0, pattern Proper (Permutation.Permutation (A:=?META1089) ==> Permutation.Permutation (A:=?META1089)) (List.rev (A:=?META1089)), id 0) simple apply Permutation.Permutation_app'(level 0, pattern Proper (Permutation.Permutation (A:=?META1087) ==> Permutation.Permutation (A:=?META1087) ==> Permutation.Permutation (A:=?META1087)) (app (A:=?META1087)), id 0) simple apply Permutation.Permutation_in'(level 0, pattern Proper (respectful eq (Permutation.Permutation (A:=?META1085) ==> iff)) (List.In (A:=?META1085)), id 0) simple apply Permutation.Permutation_cons(level 0, pattern Proper (respectful eq (Permutation.Permutation (A:=?META1083) ==> Permutation.Permutation (A:=?META1083))) cons, id 0) exact Qreduction.Qminus'_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qminus', id 0) exact Qreduction.Qmult'_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qmult', id 0) exact Qreduction.Qplus'_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qplus', id 0) exact Qreduction.Qred_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qred, id 0) exact QArith_base.Qpower_comp(level 0, pattern Proper (QArith_base.Qeq ==> eq ==> QArith_base.Qeq) QArith_base.Qpower, id 0) exact QArith_base.Qpower_positive_comp(level 0, pattern Proper (QArith_base.Qeq ==> eq ==> QArith_base.Qeq) QArith_base.Qpower_positive, id 0) exact QArith_base.Qleb_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> eq) QArith_base.Qle_bool, id 0) exact QArith_base.Qeqb_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> eq) QArith_base.Qeq_bool, id 0) exact QArith_base.Qlt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) exact QArith_base.Qle_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qle, id 0) exact QArith_base.Qcompare_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> eq) QArith_base.Qcompare, id 0) exact QArith_base.Qdiv_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qdiv, id 0) exact QArith_base.Qinv_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qinv, id 0) exact QArith_base.Qmult_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qmult, id 0) exact QArith_base.Qminus_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qminus, id 0) exact QArith_base.Qopp_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qopp, id 0) exact QArith_base.Qplus_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qplus, id 0) exact Z.ones_wd(level 0, pattern Proper (eq ==> eq) Z.ones, id 0) exact Z.lnot_wd(level 0, pattern Proper (eq ==> eq) Z.lnot, id 0) exact Z.clearbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.clearbit, id 0) exact Z.setbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.setbit, id 0) exact Z.ldiff_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.ldiff, id 0) exact Z.lor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.lor, id 0) exact Z.land_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.land, id 0) exact Z.lxor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.lxor, id 0) exact Z.div2_wd(level 0, pattern Proper (eq ==> eq) Z.div2, id 0) exact Z.shiftl_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.shiftl, id 0) exact Z.shiftr_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.shiftr, id 0) exact Z.testbit_eqf(level 0, pattern Proper (eq ==> Z.eqf) Z.testbit, id 0) exact Z.b2z_wd(level 0, pattern Proper (eq ==> eq) Z.b2z, id 0) exact Z.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) Z.eqb, id 0) exact Z.lcm_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.lcm, id 0) exact Z.Bezout_wd(level 0, pattern Proper (eq ==> eq ==> eq ==> iff) Z.Bezout, id 0) exact Z.gcd_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.gcd, id 0) exact Z.divide_wd(level 0, pattern Proper (eq ==> eq ==> iff) Z.divide, id 0) exact Z.log2_up_wd(level 0, pattern Proper (eq ==> eq) Z.log2_up, id 0) exact Z.log2_wd(level 0, pattern Proper (eq ==> eq) Z.log2, id 0) exact Z.sqrt_up_wd(level 0, pattern Proper (eq ==> eq) Z.sqrt_up, id 0) exact Z.sqrt_wd(level 0, pattern Proper (eq ==> eq) Z.sqrt, id 0) exact Z.odd_wd(level 0, pattern Proper (eq ==> eq) Z.odd, id 0) exact Z.even_wd(level 0, pattern Proper (eq ==> eq) Z.even, id 0) exact Z.Odd_wd(level 0, pattern Proper (eq ==> iff) Z.Odd, id 0) exact Z.Even_wd(level 0, pattern Proper (eq ==> iff) Z.Even, id 0) exact Z.sgn_wd(level 0, pattern Proper (eq ==> eq) Z.sgn, id 0) exact Z.abs_wd(level 0, pattern Proper (eq ==> eq) Z.abs, id 0) exact Z.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) Z.min, id 0) exact Z.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) Z.max, id 0) exact Z.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) Z.le, id 0) exact Z.le_wd(level 0, pattern Proper (eq ==> eq ==> iff) Z.le, id 0) exact N.lnot_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lnot, id 0) exact N.ones_wd(level 0, pattern Proper (eq ==> eq) N.ones, id 0) exact N.clearbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.clearbit, id 0) exact N.setbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.setbit, id 0) exact N.ldiff_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.ldiff, id 0) exact N.lor_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lor, id 0) exact N.land_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.land, id 0) exact N.lxor_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lxor, id 0) exact N.div2_wd(level 0, pattern Proper (eq ==> eq) N.div2, id 0) exact N.shiftl_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.shiftl, id 0) exact N.shiftr_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.shiftr, id 0) exact N.testbit_eqf(level 0, pattern Proper (eq ==> N.eqf) N.testbit, id 0) exact N.b2n_proper(level 0, pattern Proper (eq ==> eq) N.b2n, id 0) exact N.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) N.eqb, id 0) exact N.lcm_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lcm, id 0) exact N.Bezout_wd(level 0, pattern Proper (eq ==> eq ==> eq ==> iff) N.Bezout, id 0) exact N.gcd_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.gcd, id 0) exact N.divide_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.divide, id 0) exact N.log2_up_wd(level 0, pattern Proper (eq ==> eq) N.log2_up, id 0) exact N.log2_wd(level 0, pattern Proper (eq ==> eq) N.log2, id 0) exact N.sqrt_up_wd(level 0, pattern Proper (eq ==> eq) N.sqrt_up, id 0) exact N.Private_NZSqrt.sqrt_wd(level 0, pattern Proper (eq ==> eq) N.sqrt, id 0) exact N.odd_wd(level 0, pattern Proper (eq ==> eq) N.odd, id 0) exact N.even_wd(level 0, pattern Proper (eq ==> eq) N.even, id 0) exact N.Odd_wd(level 0, pattern Proper (eq ==> iff) N.Odd, id 0) exact N.Even_wd(level 0, pattern Proper (eq ==> iff) N.Even, id 0) exact N.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) N.min, id 0) exact N.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) N.max, id 0) exact N.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) N.le, id 0) exact N.lt_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.lt_alt, id 0) exact N.le_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.le_alt, id 0) exact N.le_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.le, id 0) simple apply @N.recursion_wd(level 0, pattern Proper (respectful ?META763 ((eq ==> respectful ?META763 ?META763) ==> respectful eq ?META763)) N.recursion, id 0) exact Pos.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) Pos.min, id 0) exact Pos.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) Pos.max, id 0) exact Pos.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) Pos.le, id 0) exact Pos.lt_compat(level 0, pattern Proper (eq ==> eq ==> iff) Pos.lt, id 0) exact Pos.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) Pos.eqb, id 0) exact Nat.lnot_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lnot, id 0) exact Nat.ones_wd(level 0, pattern Proper (eq ==> eq) Nat.ones, id 0) exact Nat.clearbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.clearbit, id 0) exact Nat.setbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.setbit, id 0) exact Nat.ldiff_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.ldiff, id 0) exact Nat.lor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lor, id 0) exact Nat.land_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.land, id 0) exact Nat.lxor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lxor, id 0) exact Nat.div2_wd(level 0, pattern Proper (eq ==> eq) Nat.div2, id 0) exact Nat.shiftl_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.shiftl, id 0) exact Nat.shiftr_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.shiftr, id 0) exact Nat.testbit_eqf(level 0, pattern Proper (eq ==> Nat.eqf) Nat.testbit, id 0) exact Nat.b2n_proper(level 0, pattern Proper (eq ==> eq) Nat.b2n, id 0) exact Nat.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) Nat.eqb, id 0) exact Nat.lcm_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lcm, id 0) exact Nat.Bezout_wd(level 0, pattern Proper (eq ==> eq ==> eq ==> iff) Nat.Bezout, id 0) exact Nat.gcd_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.gcd, id 0) exact Nat.divide_wd(level 0, pattern Proper (eq ==> eq ==> iff) Nat.divide, id 0) exact Nat.log2_up_wd(level 0, pattern Proper (eq ==> eq) Nat.log2_up, id 0) exact Nat.log2_wd(level 0, pattern Proper (eq ==> eq) Nat.log2, id 0) exact Nat.sqrt_up_wd(level 0, pattern Proper (eq ==> eq) Nat.sqrt_up, id 0) exact Nat.Private_NZSqrt.sqrt_wd(level 0, pattern Proper (eq ==> eq) Nat.sqrt, id 0) exact Nat.odd_wd(level 0, pattern Proper (eq ==> eq) Nat.odd, id 0) exact Nat.even_wd(level 0, pattern Proper (eq ==> eq) Nat.even, id 0) exact Nat.Odd_wd(level 0, pattern Proper (eq ==> iff) Nat.Odd, id 0) exact Nat.Even_wd(level 0, pattern Proper (eq ==> iff) Nat.Even, id 0) exact Nat.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) Nat.min, id 0) exact Nat.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) Nat.max, id 0) exact Nat.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) le, id 0) exact Nat.lt_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) Nat.lt_alt, id 0) exact Nat.le_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) Nat.le_alt, id 0) exact Nat.le_wd(level 0, pattern Proper (eq ==> eq ==> iff) le, id 0) simple apply @Nat.recursion_wd(level 0, pattern Proper (respectful ?META686 ((eq ==> respectful ?META686 ?META686) ==> respectful eq ?META686)) Nat.recursion, id 0) exact Nat.testbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.testbit, id 0) exact Nat.lt_wd(level 0, pattern Proper (eq ==> eq ==> iff) lt, id 0) exact Nat.mod_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.modulo, id 0) exact Nat.div_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.div, id 0) exact Nat.pow_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.pow, id 0) exact Nat.mul_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.mul, id 0) exact Nat.sub_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.sub, id 0) exact Nat.add_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.add, id 0) exact Nat.pred_wd(level 0, pattern Proper (eq ==> eq) Init.Nat.pred, id 0) exact Nat.succ_wd(level 0, pattern Proper (eq ==> eq) S, id 0) simple apply @Morphisms_Prop.well_founded_morphism(level 0, pattern Proper (relation_equivalence ==> iff) (well_founded (A:=?META733)), id 0) simple apply @Morphisms_Prop.Acc_rel_morphism(level 0, pattern Proper (relation_equivalence ==> respectful eq iff) (Acc (A:=?META731)), id 0) simple apply @Morphisms_Prop.all_iff_morphism(level 0, pattern Proper (pointwise_relation ?META691 iff ==> iff) (all (A:=?META691)), id 0) simple apply @Morphisms_Prop.ex_iff_morphism(level 0, pattern Proper (pointwise_relation ?META559 iff ==> iff) (ex (A:=?META559)), id 0) exact Morphisms_Prop.iff_iff_iff_impl_morphism(level 0, pattern Proper (iff ==> iff ==> iff) Basics.impl, id 0) exact Morphisms_Prop.or_iff_morphism(level 0, pattern Proper (iff ==> iff ==> iff) or, id 0) exact Morphisms_Prop.and_iff_morphism(level 0, pattern Proper (iff ==> iff ==> iff) and, id 0) exact Morphisms_Prop.not_iff_morphism(level 0, pattern Proper (iff ==> iff) not, id 0) simple apply @proper_proper(level 0, pattern Proper (relation_equivalence ==> respectful eq iff) Proper, id 0) simple apply @respectful_morphism(level 0, pattern Proper (relation_equivalence ==> relation_equivalence ==> relation_equivalence) respectful, id 0) simple apply @compose_proper(level 0, pattern Proper (respectful ?META348 ?META349 ==> respectful ?META347 ?META348 ==> respectful ?META347 ?META349) Basics.compose, id 0) simple apply @proper_subrelation_proper(level 0, pattern Proper (subrelation ==> respectful eq Basics.impl) Proper, id 0) simple apply SetoidList.equivlistA_app_proper(level 1, pattern Proper (SetoidList.equivlistA ?META792 ==> SetoidList.equivlistA ?META792 ==> SetoidList.equivlistA ?META792) (app (A:=?META791)), id 0) simple apply SetoidList.equivlistA_cons_proper(level 1, pattern Proper (respectful ?META786 (SetoidList.equivlistA ?META786 ==> SetoidList.equivlistA ?META786)) cons, id 0) simple apply SetoidList.InA_compat(level 1, pattern Proper (respectful ?META780 (SetoidList.equivlistA ?META780 ==> iff)) (SetoidList.InA ?META780), id 0) simple apply @Morphisms_Prop.all_flip_impl_morphism(level 1, pattern Proper (pointwise_relation ?META719 (Basics.flip Basics.impl) ==> Basics.flip Basics.impl) (all (A:=?META719)), id 0) simple apply @Morphisms_Prop.all_impl_morphism(level 1, pattern Proper (pointwise_relation ?META705 Basics.impl ==> Basics.impl) (all (A:=?META705)), id 0) simple apply @Morphisms_Prop.ex_flip_impl_morphism(level 1, pattern Proper (pointwise_relation ?META635 (Basics.flip Basics.impl) ==> Basics.flip Basics.impl) (ex (A:=?META635)), id 0) simple apply @Morphisms_Prop.ex_impl_morphism(level 1, pattern Proper (pointwise_relation ?META597 Basics.impl ==> Basics.impl) (ex (A:=?META597)), id 0) exact Morphisms_Prop.or_impl_morphism(level 1, pattern Proper (Basics.impl ==> Basics.impl ==> Basics.impl) or, id 0) exact Morphisms_Prop.and_impl_morphism(level 1, pattern Proper (Basics.impl ==> Basics.impl ==> Basics.impl) and, id 0) exact Morphisms_Prop.not_impl_morphism(level 1, pattern Proper (Basics.impl --> Basics.impl) not, id 0) (*external*) (apply @flip_proper)(level 1, pattern Proper _ (Basics.flip _), id 0) (*external*) (apply @complement_proper)(level 1, pattern Proper _ (complement _), id 0) simple apply @PER_morphism(level 1, pattern Proper (respectful ?META339 (respectful ?META339 iff)) ?META339, id 0) simple apply @trans_contra_co_morphism(level 1, pattern Proper (respectful (Basics.flip ?META287) (respectful ?META287 Basics.impl)) ?META287, id 0) simple apply @subrelation_id_proper(level 1, pattern Proper (respectful ?META267 ?META268) id, id 0) simple apply SetoidList.InfA_compat(level 2, pattern Proper (respectful ?META798 (SetoidList.eqlistA ?META798 ==> iff)) (Sorted.HdRel ?META800), id 0) simple apply @Morphisms_Prop.Acc_pt_morphism(level 2, pattern Proper (respectful ?META722 iff) (Acc ?META723), id 0) (*external*) (class_apply @proper_flip_proper)(level 2, pattern Proper (Basics.flip _) _, id 0) simple apply @trans_co_eq_inv_impl_morphism(level 2, pattern Proper (respectful ?META333 (respectful eq (Basics.flip Basics.impl))) ?META333, id 0) simple apply @per_partial_app_morphism(level 2, pattern Proper (respectful ?META325 iff) (?META325 ?META327), id 0) simple eapply @PartialOrder_proper(level 3, pattern Proper (respectful ?META371 (respectful ?META371 iff)) ?META373, id 0) simple apply @trans_sym_contra_impl_morphism(level 3, pattern Proper (respectful (Basics.flip ?META317) Basics.impl) (?META317 ?META319), id 0) simple apply @trans_sym_co_inv_impl_morphism(level 3, pattern Proper (respectful ?META309 (Basics.flip Basics.impl)) (?META309 ?META311), id 0) simple apply @trans_co_impl_morphism(level 3, pattern Proper (respectful ?META301 Basics.impl) (?META301 ?META303), id 0) simple apply @trans_contra_inv_impl_morphism(level 3, pattern Proper (respectful (Basics.flip ?META293) (Basics.flip Basics.impl)) (?META293 ?META295), id 0) (*external*) partial_application_tactic(level 4, pattern Proper _ _, id 0) (*external*) proper_subrelation(level 5, pattern Proper ?H _, id 0) (*external*) proper_normalization(level 6, pattern Proper _ _, id 0) (*external*) proper_reflexive(level 7, pattern Proper _ _, id 0) exact Permutation.Permutation_list_max(level 10, pattern Proper (Permutation.Permutation (A:=nat) ==> eq) List.list_max, id 0) exact Permutation.Permutation_list_sum(level 10, pattern Proper (Permutation.Permutation (A:=nat) ==> eq) List.list_sum, id 0) simple apply Permutation.Permutation_length'(level 10, pattern Proper (Permutation.Permutation (A:=?META1091) ==> eq) (length (A:=?META1091)), id 0) For Asymmetric -> simple apply @StrictOrder_Asymmetric(level 1, pattern Asymmetric ?META233, id 0) (*external*) (class_apply @flip_Asymmetric)(level 3, pattern Asymmetric (Basics.flip _), id 0) For Irreflexive -> simple apply @StrictOrder_Irreflexive(level 1, pattern Irreflexive ?META221, id 0) (*external*) (class_apply @flip_Irreflexive)(level 3, pattern Irreflexive (Basics.flip _), id 0) (*external*) (class_apply @complement_Irreflexive)(level 3, pattern Irreflexive (complement _), id 0) For CRelationClasses.Transitive -> exact CRelationClasses.iffT_Transitive(level 0, pattern CRelationClasses.Transitive CRelationClasses.iffT, id 0) exact CRelationClasses.arrow_Transitive(level 0, pattern CRelationClasses.Transitive CRelationClasses.arrow, id 0) exact CRelationClasses.iff_Transitive(level 0, pattern CRelationClasses.Transitive iff, id 0) exact CRelationClasses.impl_Transitive(level 0, pattern CRelationClasses.Transitive Basics.impl, id 0) simple apply @CRelationClasses.eq_Transitive(level 0, pattern CRelationClasses.Transitive eq, id 0) simple apply @CRelationClasses.Equivalence_Transitive(level 1, pattern CRelationClasses.Transitive ?META215, id 0) simple apply @CRelationClasses.StrictOrder_Transitive(level 1, pattern CRelationClasses.Transitive ?META179, id 0) simple apply @CRelationClasses.PreOrder_Transitive(level 2, pattern CRelationClasses.Transitive ?META167, id 0) (*external*) ( class_apply @CRelationClasses.flip_Transitive)(level 3, pattern CRelationClasses.Transitive (CRelationClasses.flip _), id 0) simple apply @CRelationClasses.PER_Transitive(level 3, pattern CRelationClasses.Transitive ?META197, id 0) For CMorphisms.Proper -> simple apply @CMorphisms.proper_proper(level 0, pattern CMorphisms.Proper (CMorphisms.respectful CRelationClasses.relation_equivalence (CMorphisms.respectful eq CRelationClasses.iffT)) CMorphisms.Proper, id 0) simple apply @CMorphisms.respectful_morphism(level 0, pattern CMorphisms.Proper (CMorphisms.respectful CRelationClasses.relation_equivalence (CMorphisms.respectful CRelationClasses.relation_equivalence CRelationClasses.relation_equivalence)) CMorphisms.respectful, id 0) simple apply CMorphisms.compose_proper(level 0, pattern CMorphisms.Proper (CMorphisms.respectful (CMorphisms.respectful ?META294 ?META295) (CMorphisms.respectful (CMorphisms.respectful ?META293 ?META294) (CMorphisms.respectful ?META293 ?META295))) Basics.compose, id 0) simple apply @CMorphisms.proper_subrelation_proper_arrow(level 0, pattern CMorphisms.Proper (CMorphisms.respectful CRelationClasses.subrelation (CMorphisms.respectful eq CRelationClasses.arrow)) CMorphisms.Proper, id 0) (*external*) (apply @CMorphisms.flip_proper)(level 1, pattern CMorphisms.Proper _ (CRelationClasses.flip _), id 0) simple apply @CMorphisms.PER_type_morphism(level 1, pattern CMorphisms.Proper (CMorphisms.respectful ?META285 (CMorphisms.respectful ?META285 CRelationClasses.iffT)) ?META285, id 0) simple apply @CMorphisms.trans_contra_co_type_morphism(level 1, pattern CMorphisms.Proper (CMorphisms.respectful (CRelationClasses.flip ?META233) (CMorphisms.respectful ?META233 CRelationClasses.arrow)) ?META233, id 0) simple apply @CMorphisms.subrelation_id_proper(level 1, pattern CMorphisms.Proper (CMorphisms.respectful ?META213 ?META214) id, id 0) (*external*) (class_apply @CMorphisms.proper_flip_proper)(level 2, pattern CMorphisms.Proper (CRelationClasses.flip _) _, id 0) simple apply @CMorphisms.trans_co_eq_inv_arrow_morphism(level 2, pattern CMorphisms.Proper (CMorphisms.respectful ?META279 (CMorphisms.respectful eq (CRelationClasses.flip CRelationClasses.arrow))) ?META279, id 0) simple apply @CMorphisms.per_partial_app_type_morphism(level 2, pattern CMorphisms.Proper (CMorphisms.respectful ?META271 CRelationClasses.iffT) (?META271 ?META273), id 0) simple eapply @CMorphisms.PartialOrder_proper_type(level 3, pattern CMorphisms.Proper (CMorphisms.respectful ?META365 (CMorphisms.respectful ?META365 CRelationClasses.iffT)) ?META367, id 0) simple apply @CMorphisms.trans_sym_contra_arrow_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful (CRelationClasses.flip ?META263) CRelationClasses.arrow) (?META263 ?META265), id 0) simple apply @CMorphisms.trans_sym_co_inv_impl_type_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful ?META255 (CRelationClasses.flip CRelationClasses.arrow)) (?META255 ?META257), id 0) simple apply @CMorphisms.trans_co_impl_type_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful ?META247 CRelationClasses.arrow) (?META247 ?META249), id 0) simple apply @CMorphisms.trans_contra_inv_impl_type_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful (CRelationClasses.flip ?META239) (CRelationClasses.flip CRelationClasses.arrow)) (?META239 ?META241), id 0) (*external*) CMorphisms.partial_application_tactic(level 4, pattern CMorphisms.Proper _ _, id 0) (*external*) CMorphisms.proper_subrelation(level 5, pattern CMorphisms.Proper ?H _, id 0) (*external*) CMorphisms.proper_normalization(level 6, pattern CMorphisms.Proper _ _, id 0) (*external*) CMorphisms.proper_reflexive(level 7, pattern CMorphisms.Proper _ _, id 0) For CRelationClasses.subrelation -> (*external*) ( class_apply @CMorphisms.flip2)(level 1, pattern CRelationClasses.subrelation _ (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CMorphisms.flip1)(level 1, pattern CRelationClasses.subrelation (CRelationClasses.flip _) _, id 0) exact CMorphisms.iffT_flip_arrow_subrelation(level 2, pattern CRelationClasses.subrelation CRelationClasses.iffT (CRelationClasses.flip CRelationClasses.arrow), id 0) exact CMorphisms.iffT_arrow_subrelation(level 2, pattern CRelationClasses.subrelation CRelationClasses.iffT CRelationClasses.arrow, id 0) exact CMorphisms.iff_flip_impl_subrelation(level 2, pattern CRelationClasses.subrelation iff (CRelationClasses.flip Basics.impl), id 0) exact CMorphisms.iff_impl_subrelation(level 2, pattern CRelationClasses.subrelation iff Basics.impl, id 0) (*external*) ( CMorphisms.subrelation_tac T U)(level 3, pattern CRelationClasses.subrelation ?T ?U, id 0) (*external*) ( apply (CMorphisms.forall_subrelation B R S); intro)(level 4, pattern CRelationClasses.subrelation (CMorphisms.forall_relation ?R) (CMorphisms.forall_relation ?S), id 0) simple apply @CMorphisms.pointwise_subrelation(level 4, pattern CRelationClasses.subrelation (CMorphisms.pointwise_relation ?META222 ?META224) (CMorphisms.pointwise_relation ?META222 ?META225), id 0) (*external*) ( class_apply @CRelationClasses.subrelation_symmetric)(level 4, pattern CRelationClasses.subrelation (CRelationClasses.flip _) _, id 0) For Transitive -> exact iff_Transitive(level 0, pattern Transitive iff, id 0) exact impl_Transitive(level 0, pattern Transitive Basics.impl, id 0) simple apply @eq_Transitive(level 0, pattern Transitive eq, id 0) simple apply @Equivalence.equiv_transitive(level 1, pattern Transitive Equivalence.equiv, id 0) simple apply @Equivalence_Transitive(level 1, pattern Transitive ?META263, id 0) simple apply @StrictOrder_Transitive(level 1, pattern Transitive ?META227, id 0) simple apply @PreOrder_Transitive(level 2, pattern Transitive ?META215, id 0) (*external*) (class_apply @flip_Transitive)(level 3, pattern Transitive (Basics.flip _), id 0) simple apply @PER_Transitive(level 3, pattern Transitive ?META245, id 0) exact Z.divide_transitive(level 5, pattern Transitive Z.divide, id 0) exact N.divide_transitive(level 5, pattern Transitive N.divide, id 0) exact Nat.divide_transitive(level 5, pattern Transitive Nat.divide, id 0) simple apply @Equivalence.pointwise_transitive(level 9, pattern Transitive (pointwise_relation ?META419 ?META421), id 0) For CRelationClasses.PartialOrder -> (*external*) ( class_apply @CRelationClasses.PartialOrder_inverse)(level 3, pattern CRelationClasses.PartialOrder (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CMorphisms.StrictOrder_PartialOrder)(level 4, pattern CRelationClasses.PartialOrder _ (CRelationClasses.relation_disjunction _ _), id 0) For subrelation -> simple apply SetoidList.eqlistA_equivlistA(level 1, pattern subrelation (SetoidList.eqlistA ?META774) (SetoidList.equivlistA ?META774), id 0) (*external*) (class_apply @flip2)(level 1, pattern subrelation _ (Basics.flip _), id 0) (*external*) (class_apply @flip1)(level 1, pattern subrelation (Basics.flip _) _, id 0) exact iff_flip_impl_subrelation(level 2, pattern subrelation iff (Basics.flip Basics.impl), id 0) exact iff_impl_subrelation(level 2, pattern subrelation iff Basics.impl, id 0) (*external*) (subrelation_tac T U)(level 3, pattern subrelation ?T ?U, id 0) (*external*) (apply (forall_subrelation B R S); intro)(level 4, pattern subrelation (forall_relation ?R) (forall_relation ?S), id 0) simple apply @pointwise_subrelation(level 4, pattern subrelation (pointwise_relation ?META276 ?META278) (pointwise_relation ?META276 ?META279), id 0) (*external*) (class_apply @subrelation_symmetric)(level 4, pattern subrelation (Basics.flip _) _, id 0) For Normalizes -> (*external*) normalizes(level 1, pattern Normalizes _ _ _, id 0) For Idempotent -> exact aac_Zmax_Idem(level 0, pattern Idempotent eq BinIntDef.Z.max, id 0) exact aac_Zmin_Idem(level 0, pattern Idempotent eq BinIntDef.Z.min, id 0) For ProperProxy -> (*external*) (class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy)(level 1, pattern ProperProxy _ _, id 0) (*external*) (not_evar R; class_apply @proper_proper_proxy)(level 2, pattern ProperProxy ?R _, id 0) For PartialOrder -> exact Z.le_partialorder(level 0, pattern PartialOrder eq Z.le, id 0) exact N.le_partialorder(level 0, pattern PartialOrder eq N.le, id 0) exact Pos.le_partorder(level 0, pattern PartialOrder eq Pos.le, id 0) exact Nat.le_partialorder(level 0, pattern PartialOrder eq le, id 0) simple apply @subrelation_partial_order(level 0, pattern PartialOrder relation_equivalence subrelation, id 0) (*external*) (class_apply @PartialOrder_inverse)(level 3, pattern PartialOrder (Basics.flip _), id 0) (*external*) (class_apply @StrictOrder_PartialOrder)(level 4, pattern PartialOrder _ (relation_disjunction _ _), id 0) For CRelationClasses.Symmetric -> exact CRelationClasses.iffT_Symmetric(level 0, pattern CRelationClasses.Symmetric CRelationClasses.iffT, id 0) exact CRelationClasses.iff_Symmetric(level 0, pattern CRelationClasses.Symmetric iff, id 0) simple apply @CRelationClasses.eq_Symmetric(level 0, pattern CRelationClasses.Symmetric eq, id 0) simple apply @CRelationClasses.Equivalence_Symmetric(level 1, pattern CRelationClasses.Symmetric ?META209, id 0) (*external*) ( class_apply @CRelationClasses.flip_Symmetric)(level 3, pattern CRelationClasses.Symmetric (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CRelationClasses.complement_Symmetric)(level 3, pattern CRelationClasses.Symmetric (CRelationClasses.complement _), id 0) simple apply @CRelationClasses.PER_Symmetric(level 3, pattern CRelationClasses.Symmetric ?META191, id 0) For CRelationClasses.Antisymmetric -> simple eapply @CRelationClasses.partial_order_antisym(level 2, pattern CRelationClasses.Antisymmetric ?META265 ?META267, id 0) (*external*) ( class_apply @CRelationClasses.flip_Antisymmetric)(level 3, pattern CRelationClasses.Antisymmetric (CRelationClasses.flip _), id 0) For ZifyClasses.BinRel -> exact ZifyInst.Op_eqZ(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_Z_le(level 0, pattern ZifyClasses.BinRel Z.le, id 0) exact ZifyInst.Op_Z_gt(level 0, pattern ZifyClasses.BinRel Z.gt, id 0) exact ZifyInst.Op_Z_lt(level 0, pattern ZifyClasses.BinRel Z.lt, id 0) exact ZifyInst.Op_Z_ge(level 0, pattern ZifyClasses.BinRel Z.ge, id 0) exact ZifyInst.Op_eq_N(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_N_le(level 0, pattern ZifyClasses.BinRel N.le, id 0) exact ZifyInst.Op_N_gt(level 0, pattern ZifyClasses.BinRel N.gt, id 0) exact ZifyInst.Op_N_lt(level 0, pattern ZifyClasses.BinRel N.lt, id 0) exact ZifyInst.Op_N_ge(level 0, pattern ZifyClasses.BinRel N.ge, id 0) exact ZifyInst.Op_eq_pos(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_pos_le(level 0, pattern ZifyClasses.BinRel Pos.le, id 0) exact ZifyInst.Op_pos_gt(level 0, pattern ZifyClasses.BinRel Pos.gt, id 0) exact ZifyInst.Op_pos_lt(level 0, pattern ZifyClasses.BinRel Pos.lt, id 0) exact ZifyInst.Op_pos_ge(level 0, pattern ZifyClasses.BinRel Pos.ge, id 0) exact ZifyInst.Op_Nat_eq(level 0, pattern ZifyClasses.BinRel Nat.eq, id 0) exact ZifyInst.Op_eq_nat(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_Nat_le(level 0, pattern ZifyClasses.BinRel Nat.le, id 0) exact ZifyInst.Op_le(level 0, pattern ZifyClasses.BinRel le, id 0) exact ZifyInst.Op_gt(level 0, pattern ZifyClasses.BinRel gt, id 0) exact ZifyInst.Op_Nat_lt(level 0, pattern ZifyClasses.BinRel Nat.lt, id 0) exact ZifyInst.Op_lt(level 0, pattern ZifyClasses.BinRel lt, id 0) exact ZifyInst.Op_ge(level 0, pattern ZifyClasses.BinRel ge, id 0) For SetoidTactics.DefaultRelation -> simple apply @SetoidTactics.equivalence_default(level 4, pattern SetoidTactics.DefaultRelation ?META473, id 0) For ZifyClasses.InjTyp -> exact ZifyInst.Inj_N_Z(level 0, pattern ZifyClasses.InjTyp N Z, id 0) exact ZifyInst.Inj_pos_Z(level 0, pattern ZifyClasses.InjTyp positive Z, id 0) exact ZifyInst.Inj_nat_Z(level 0, pattern ZifyClasses.InjTyp nat Z, id 0) exact ZifyInst.Inj_Z_Z(level 0, pattern ZifyClasses.InjTyp Z Z, id 0) For CRelationClasses.PreOrder -> simple apply @CRelationClasses.relation_implication_preorder(level 0, pattern CRelationClasses.PreOrder CRelationClasses.subrelation, id 0) (*external*) (class_apply @CRelationClasses.flip_PreOrder)(level 3, pattern CRelationClasses.PreOrder (CRelationClasses.flip _), id 0) (*external*) (class_apply @CMorphisms.StrictOrder_PreOrder)(level 4, pattern CRelationClasses.PreOrder (CRelationClasses.relation_disjunction _ _), id 0) For CRelationClasses.Equivalence -> simple apply @CRelationClasses.relation_equivalence_equivalence(level 0, pattern CRelationClasses.Equivalence CRelationClasses.relation_equivalence, id 0) exact CRelationClasses.iff_equivalence(level 0, pattern CRelationClasses.Equivalence iff, id 0) simple apply @CRelationClasses.eq_equivalence(level 10, pattern CRelationClasses.Equivalence eq, id 0) For PreOrder -> exact preorder_Zle(level 0, pattern PreOrder Z.le, id 0) exact Z.le_preorder(level 0, pattern PreOrder Z.le, id 0) exact N.le_preorder(level 0, pattern PreOrder N.le, id 0) exact Pos.le_preorder(level 0, pattern PreOrder Pos.le, id 0) exact Nat.le_preorder(level 0, pattern PreOrder le, id 0) simple apply @relation_implication_preorder(level 0, pattern PreOrder subrelation, id 0) simple apply @predicate_implication_preorder(level 0, pattern PreOrder predicate_implication, id 0) (*external*) (class_apply @flip_PreOrder)(level 3, pattern PreOrder (Basics.flip _), id 0) (*external*) (class_apply @StrictOrder_PreOrder)(level 4, pattern PreOrder (relation_disjunction _ _), id 0) simple apply @Equivalence_PreOrder(level 10, pattern PreOrder ?META275, id 0) For CRelationClasses.PER -> simple apply @CRelationClasses.Equivalence_PER(level 10, pattern CRelationClasses.PER ?META221, id 0) For ZifyClasses.BinOpSpec -> exact ZifyInst.ZminSpec(level 0, pattern ZifyClasses.BinOpSpec BinIntDef.Z.min, id 0) exact ZifyInst.ZmaxSpec(level 0, pattern ZifyClasses.BinOpSpec BinIntDef.Z.max, id 0) For Equivalence -> exact Qminmax.Q.OT.eq_equiv(level 0, pattern Equivalence QArith_base.Qeq, id 0) exact QOrderedType.QOrder.TO.eq_equiv(level 0, pattern Equivalence QArith_base.Qeq, id 0) simple apply FMapPositive.PositiveMap.eqke_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.eq_key_elt (A:=?META1651)), id 0) simple apply FMapPositive.PositiveMap.eqk_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.eq_key (A:=?META1649)), id 0) simple apply FMapPositive.PositiveMap.ME.eqke_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.ME.eqke (elt:=?META917)), id 0) simple apply FMapPositive.PositiveMap.ME.eqk_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.ME.eqk (elt:=?META915)), id 0) exact FMapPositive.PositiveMap.ME.MO.eq_equiv(level 0, pattern Equivalence eq, id 0) simple apply Permutation.Permutation_Equivalence(level 0, pattern Equivalence (Permutation.Permutation (A:=?META1081)), id 0) exact QArith_base.Q_Setoid(level 0, pattern Equivalence QArith_base.Qeq, id 0) exact Ndigits.eqf_equiv(level 0, pattern Equivalence Ndigits.eqf, id 0) exact Z.eqf_equiv(level 0, pattern Equivalence Z.eqf, id 0) exact N.eqf_equiv(level 0, pattern Equivalence N.eqf, id 0) exact Nat.eqf_equiv(level 0, pattern Equivalence Nat.eqf, id 0) simple apply @relation_equivalence_equivalence(level 0, pattern Equivalence relation_equivalence, id 0) simple apply @predicate_equivalence_equivalence(level 0, pattern Equivalence predicate_equivalence, id 0) exact iff_equivalence(level 0, pattern Equivalence iff, id 0) simple apply SetoidList.eqlistA_equiv(level 1, pattern Equivalence (SetoidList.eqlistA ?META768), id 0) simple apply SetoidList.equivlist_equiv(level 1, pattern Equivalence (SetoidList.equivlistA ?META762), id 0) simple apply @Equivalence.pointwise_equivalence(level 9, pattern Equivalence (pointwise_relation ?META427 ?META429), id 0) simple apply @eq_equivalence(level 10, pattern Equivalence eq, id 0) simple apply Permutation.Permutation_transp_equiv(level 100, pattern Equivalence (Permutation.Permutation_transp (A:=?META1115)), id 0) For PER -> simple apply @Equivalence_PER(level 10, pattern PER ?META269, id 0) For Unit -> exact aac_zero_Zplus(level 0, pattern Unit eq BinIntDef.Z.add 0, id 0) exact aac_one(level 0, pattern Unit eq BinIntDef.Z.mul 1, id 0) For CRelationClasses.StrictOrder -> (*external*) ( class_apply @CRelationClasses.flip_StrictOrder)(level 3, pattern CRelationClasses.StrictOrder (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CMorphisms.PartialOrder_StrictOrder)(level 4, pattern CRelationClasses.StrictOrder (CRelationClasses.relation_conjunction _ _), id 0) For ZifyClasses.Saturate -> exact ZifyInst.SatPowNonneg(level 0, pattern ZifyClasses.Saturate BinIntDef.Z.pow, id 0) exact ZifyInst.SatPowPos(level 0, pattern ZifyClasses.Saturate BinIntDef.Z.pow, id 0) For AAC_lift -> exact lift_le_eq(level 0, pattern AAC_lift Z.le eq, id 0) simple apply @aac_lift_subrelation(level 3, pattern AAC_lift ?META1678 ?META1679, id 0) simple apply @aac_lift_proper(level 4, pattern AAC_lift ?META1690 ?META1691, id 0) For DeclConstant.GT -> simple apply @DeclConstant.GT_O(level 1, pattern DeclConstant.GT ?META727, id 0) simple apply @DeclConstant.GT_APP1(level 2, pattern DeclConstant.GT (?META734 ?META735), id 0) simple apply @DeclConstant.GT_APP2(level 3, pattern DeclConstant.GT (?META747 ?META748 ?META749), id 0) For CRelationClasses.RewriteRelation -> simple apply @CRelationClasses.RewriteRelation_instance_2(level 0, pattern CRelationClasses.RewriteRelation CRelationClasses.relation_equivalence, id 0) exact CRelationClasses.RewriteRelation_instance_1(level 0, pattern CRelationClasses.RewriteRelation iff, id 0) exact CRelationClasses.RewriteRelation_instance_0(level 0, pattern CRelationClasses.RewriteRelation Basics.impl, id 0) simple apply @CRelationClasses.equivalence_rewrite_crelation(level 1, pattern CRelationClasses.RewriteRelation ?META227, id 0) For StrictOrder -> exact Qminmax.Q.OT.lt_strorder(level 0, pattern StrictOrder QArith_base.Qlt, id 0) exact QOrderedType.QOrder.TO.lt_strorder(level 0, pattern StrictOrder QArith_base.Qlt, id 0) exact QOrderedType.Q_as_OT.lt_strorder(level 0, pattern StrictOrder QArith_base.Qlt, id 0) simple apply FMapPositive.PositiveMap.ltk_strorder(level 0, pattern StrictOrder (FMapPositive.PositiveMap.lt_key (A:=?META1653)), id 0) simple apply FMapPositive.PositiveMap.ME.ltk_strorder(level 0, pattern StrictOrder (FMapPositive.PositiveMap.ME.ltk (elt:=?META919)), id 0) exact FMapPositive.PositiveMap.ME.MO.lt_strorder(level 0, pattern StrictOrder OrderedTypeEx.PositiveOrderedTypeBits.bits_lt, id 0) exact Z.lt_strorder(level 0, pattern StrictOrder Z.lt, id 0) exact N.lt_strorder(level 0, pattern StrictOrder N.lt, id 0) exact Pos.lt_strorder(level 0, pattern StrictOrder Pos.lt, id 0) exact Nat.lt_strorder(level 0, pattern StrictOrder lt, id 0) (*external*) (class_apply @flip_StrictOrder)(level 3, pattern StrictOrder (Basics.flip _), id 0) (*external*) (class_apply @PartialOrder_StrictOrder)(level 4, pattern StrictOrder (relation_conjunction _ _), id 0) For ZifyClasses.UnOpSpec -> exact ZifyInst.ZabsSpec(level 0, pattern ZifyClasses.UnOpSpec BinIntDef.Z.abs, id 0) exact ZifyInst.ZsgnSpec(level 0, pattern ZifyClasses.UnOpSpec BinIntDef.Z.sgn, id 0) For DeclConstant.DeclaredConstant -> exact DeclConstant.DQ(level 0, pattern DeclConstant.DeclaredConstant QArith_base.Qmake, id 0) exact DeclConstant.DZpow(level 0, pattern DeclConstant.DeclaredConstant BinIntDef.Z.pow, id 0) exact DeclConstant.DZpow_pos(level 0, pattern DeclConstant.DeclaredConstant BinIntDef.Z.pow_pos, id 0) exact DeclConstant.DZneg(level 0, pattern DeclConstant.DeclaredConstant (-1), id 0) exact DeclConstant.DZpos(level 0, pattern DeclConstant.DeclaredConstant Z.pos, id 0) exact DeclConstant.DZO(level 0, pattern DeclConstant.DeclaredConstant 0, id 0) exact DeclConstant.DxO(level 0, pattern DeclConstant.DeclaredConstant xO, id 0) exact DeclConstant.DxI(level 0, pattern DeclConstant.DeclaredConstant xI, id 0) exact DeclConstant.DxH(level 0, pattern DeclConstant.DeclaredConstant 1%positive, id 0) exact DeclConstant.DS(level 0, pattern DeclConstant.DeclaredConstant S, id 0) exact DeclConstant.DO(level 0, pattern DeclConstant.DeclaredConstant 0%nat, id 0) For RewriteRelation -> simple apply @RewriteRelation_instance_2(level 0, pattern RewriteRelation relation_equivalence, id 0) exact RewriteRelation_instance_1(level 0, pattern RewriteRelation iff, id 0) exact RewriteRelation_instance_0(level 0, pattern RewriteRelation Basics.impl, id 0) simple apply @equivalence_rewrite_relation(level 1, pattern RewriteRelation ?META281, id 0) For ZifyClasses.UnOp -> exact ZifyInst.Op_Z_to_pos(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.to_pos, id 0) exact ZifyInst.Op_Z_to_nat(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.to_nat, id 0) exact ZifyInst.Op_Z_quot2(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.quot2, id 0) exact ZifyInst.Op_Z_div2(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.div2, id 0) exact ZifyInst.Op_Z_square(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.square, id 0) exact ZifyInst.Op_Z_succ_double(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.succ_double, id 0) exact ZifyInst.Op_Z_pred_double(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.pred_double, id 0) exact ZifyInst.Op_Z_double(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.double, id 0) exact ZifyInst.Op_Z_sgn(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.sgn, id 0) exact ZifyInst.Op_Z_abs(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.abs, id 0) exact ZifyInst.Op_Z_opp(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.opp, id 0) exact ZifyInst.Op_Z_pred(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.pred, id 0) exact ZifyInst.Op_Z_succ(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.succ, id 0) exact ZifyInst.Op_N_square(level 0, pattern ZifyClasses.UnOp BinNatDef.N.square, id 0) exact ZifyInst.Op_N_div2(level 0, pattern ZifyClasses.UnOp BinNatDef.N.div2, id 0) exact ZifyInst.Op_N_succ_pos(level 0, pattern ZifyClasses.UnOp BinNatDef.N.succ_pos, id 0) exact ZifyInst.Op_N_double(level 0, pattern ZifyClasses.UnOp BinNatDef.N.double, id 0) exact ZifyInst.Op_N_succ_double(level 0, pattern ZifyClasses.UnOp BinNatDef.N.succ_double, id 0) exact ZifyInst.Op_N_succ(level 0, pattern ZifyClasses.UnOp BinNatDef.N.succ, id 0) exact ZifyInst.Op_N_pred(level 0, pattern ZifyClasses.UnOp BinNatDef.N.pred, id 0) exact ZifyInst.Op_N_pos(level 0, pattern ZifyClasses.UnOp N.pos, id 0) exact ZifyInst.Op_Z_abs_N(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.abs_N, id 0) exact ZifyInst.Op_N_of_nat(level 0, pattern ZifyClasses.UnOp BinNatDef.N.of_nat, id 0) exact ZifyInst.Op_N_Npos(level 0, pattern ZifyClasses.UnOp N.pos, id 0) exact ZifyInst.Op_Z_of_nat(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.of_nat, id 0) exact ZifyInst.Op_xI(level 0, pattern ZifyClasses.UnOp xI, id 0) exact ZifyInst.Op_xO(level 0, pattern ZifyClasses.UnOp xO, id 0) exact ZifyInst.Op_Pos_Ndouble(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.Ndouble, id 0) exact ZifyInst.Op_Pos_Nsucc_double(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.Nsucc_double, id 0) exact ZifyInst.Op_pos_square(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.square, id 0) exact ZifyInst.Op_pos_of_nat(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.of_nat, id 0) exact ZifyInst.Op_pos_of_succ_nat(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.of_succ_nat, id 0) exact ZifyInst.Op_pos_predN(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.pred_N, id 0) exact ZifyInst.Op_pos_pred(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.pred, id 0) exact ZifyInst.Op_pos_pred_double(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.pred_double, id 0) exact ZifyInst.Op_pos_succ(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.succ, id 0) exact ZifyInst.Op_Z_pos(level 0, pattern ZifyClasses.UnOp Z.pos, id 0) exact ZifyInst.Op_Z_neg(level 0, pattern ZifyClasses.UnOp (-1), id 0) exact ZifyInst.Op_Z_to_N(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.to_N, id 0) exact ZifyInst.Op_Z_of_N(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.of_N, id 0) exact ZifyInst.Op_N_to_nat(level 0, pattern ZifyClasses.UnOp BinNatDef.N.to_nat, id 0) exact ZifyInst.Op_pos_to_nat(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.to_nat, id 0) exact ZifyInst.Op_Z_abs_nat(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.abs_nat, id 0) exact ZifyInst.Op_S(level 0, pattern ZifyClasses.UnOp S, id 0) exact ZifyInst.Op_pred(level 0, pattern ZifyClasses.UnOp Init.Nat.pred, id 0) For ZifyClasses.BinOp -> exact ZifyInst.Op_Z_pow_pos(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.pow_pos, id 0) exact ZifyInst.Op_Z_pow(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.pow, id 0) exact ZifyInst.Op_Z_quot(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.quot, id 0) exact ZifyInst.Op_Z_rem(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.rem, id 0) exact ZifyInst.Op_Z_mod(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.modulo, id 0) exact ZifyInst.Op_Z_div(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.div, id 0) exact ZifyInst.Op_Z_sub(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.sub, id 0) exact ZifyInst.Op_Z_mul(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.mul, id 0) exact ZifyInst.Op_Z_max(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.max, id 0) exact ZifyInst.Op_Z_min(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.min, id 0) exact ZifyInst.Op_Z_add(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.add, id 0) exact ZifyInst.Op_N_pow(level 0, pattern ZifyClasses.BinOp BinNatDef.N.pow, id 0) exact ZifyInst.Op_N_mod(level 0, pattern ZifyClasses.BinOp BinNatDef.N.modulo, id 0) exact ZifyInst.Op_N_div(level 0, pattern ZifyClasses.BinOp BinNatDef.N.div, id 0) exact ZifyInst.Op_N_sub(level 0, pattern ZifyClasses.BinOp BinNatDef.N.sub, id 0) exact ZifyInst.Op_N_mul(level 0, pattern ZifyClasses.BinOp BinNatDef.N.mul, id 0) exact ZifyInst.Op_N_max(level 0, pattern ZifyClasses.BinOp BinNatDef.N.max, id 0) exact ZifyInst.Op_N_min(level 0, pattern ZifyClasses.BinOp BinNatDef.N.min, id 0) exact ZifyInst.Op_N_add(level 0, pattern ZifyClasses.BinOp BinNatDef.N.add, id 0) exact ZifyInst.Op_pos_pow(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.pow, id 0) exact ZifyInst.Op_pos_max(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.max, id 0) exact ZifyInst.Op_pos_min(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.min, id 0) exact ZifyInst.Op_pos_mul(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.mul, id 0) exact ZifyInst.Op_pos_sub(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.sub, id 0) exact ZifyInst.Op_pos_add_carry(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.add_carry, id 0) exact ZifyInst.Op_pos_add(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.add, id 0) exact ZifyInst.Op_max(level 0, pattern ZifyClasses.BinOp Init.Nat.max, id 0) exact ZifyInst.Op_min(level 0, pattern ZifyClasses.BinOp Init.Nat.min, id 0) exact ZifyInst.Op_mul(level 0, pattern ZifyClasses.BinOp Init.Nat.mul, id 0) exact ZifyInst.Op_sub(level 0, pattern ZifyClasses.BinOp Init.Nat.sub, id 0) exact ZifyInst.Op_plus(level 0, pattern ZifyClasses.BinOp Init.Nat.add, id 0) For ZifyClasses.CstOp -> exact ZifyInst.Op_Z_Z0(level 0, pattern ZifyClasses.CstOp 0, id 0) exact ZifyInst.Op_N_N0(level 0, pattern ZifyClasses.CstOp 0%N, id 0) exact ZifyInst.Op_xH(level 0, pattern ZifyClasses.CstOp 1%positive, id 0) exact ZifyInst.Op_O(level 0, pattern ZifyClasses.CstOp 0%nat, id 0) (lift_reflexivity (let env_sym := sigma_get {| Internal.Sym.ar := 0; Internal.Sym.value := b; Internal.Sym.morph := proper_eq b |} (sigma_add 1%positive {| Internal.Sym.ar := 0; Internal.Sym.value := a; Internal.Sym.morph := proper_eq a |} (sigma_empty Internal.Sym.pack)) in let env_bin := sigma_get {| Internal.Bin.value := Z.max; Internal.Bin.compat := Z.max_compat; Internal.Bin.assoc := aac_Zmax_Assoc; Internal.Bin.comm := Some aac_Zmax_Comm; Internal.Bin.idem := Some aac_Zmax_Idem |} (sigma_add 2%positive {| Internal.Bin.value := Z.add; Internal.Bin.compat := reflexive_proper Z.add; Internal.Bin.assoc := aac_Zplus_Assoc; Internal.Bin.comm := Some aac_Zplus_Comm; Internal.Bin.idem := None |} (sigma_empty Internal.Bin.pack)) in let env_units := sigma_get {| Internal.u_value := 0; Internal.u_desc := {| Internal.uf_idx := 2; Internal.uf_desc := aac_zero_Zplus |} :: nil |} (sigma_empty (Internal.unit_pack env_bin)) in let tty := Internal.T env_sym in let rsum := Internal.sum (e_sym:=env_sym) in let rprd := Internal.prd (e_sym:=env_sym) in let rsym := Internal.sym (e_sym:=env_sym) in let vnil := Internal.vnil env_sym in let vcons := Internal.vcons (e_sym:=env_sym) in let eval := Internal.eval (e_sym:=env_sym) env_units in let left := rsum 1%positive (Utils.cons (rsum 2%positive (Utils.cons (rsym 1%positive vnil, 1%positive) (Utils.nil (rsym 2%positive vnil, 1%positive))), 1%positive) (Utils.nil (rsum 2%positive (Utils.cons (rsym 2%positive vnil, 1%positive) (Utils.nil (rsym 1%positive vnil, 1%positive))), 1%positive))) in let right := rsum 2%positive (Utils.cons (rsym 1%positive vnil, 1%positive) (Utils.nil (rsym 2%positive vnil, 1%positive))) in Internal.decide env_units left right (eq_refl : Internal.compare (Internal.norm env_units left) (Internal.norm env_units right) = Eq) <: Z.max (a + b) (b + a) = a + b)) File "./theories/Tutorial.v", line 398, characters 4-37: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (Z.abs a + - Z.abs b + 0)%Z occurrence 1: transitivity through (Z.abs a + - (Z.abs b + 0))%Z occurrence 2: transitivity through (Z.abs a + - Z.abs (b + 0))%Z occurrence 3: transitivity through (- Z.abs b + Z.abs (a + 0))%Z File "./theories/Tutorial.v", line 399, characters 4-40: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Caveats.v All solutions: occurrence 0: transitivity through forall x : Z, (- (x + x) + (b + b + c))%Z 1 possible(s) substitution(s) 0: [x: a; ] occurrence 1: transitivity through forall x : Z, (x + x + (- (a + a) + c))%Z 1 possible(s) substitution(s) 0: [x: b; ] File "./theories/Caveats.v", line 276, characters 4-32: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through dot y 1 occurrence 1: transitivity through dot 1 y File "./theories/Caveats.v", line 277, characters 4-35: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 295, characters 4-18: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 303, characters 4-23: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 327, characters 2-19: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c * b + a + 0)%nat occurrence 1: transitivity through (a + b * (c + 0))%nat occurrence 2: transitivity through (a + c * (b + 0))%nat File "./theories/Caveats.v", line 344, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c + b + a + 0)%nat File "./theories/Caveats.v", line 347, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((c + b + a) * 1)%nat occurrence 1: transitivity through (c + a + b * 1)%nat occurrence 2: transitivity through (a + (c + b) * 1)%nat occurrence 3: transitivity through (b + a + c * 1)%nat occurrence 4: transitivity through (c + (b + a) * 1)%nat occurrence 5: transitivity through (c + b + a * 1)%nat occurrence 6: transitivity through (b + (c + a) * 1)%nat All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] File "./theories/Caveats.v", line 363, characters 2-22: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] occurrence 1: transitivity through ((a * b + a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 2: transitivity through (a * b + c + a * a * (1 * 1 + 0 * 1))%nat occurrence 3: transitivity through (c + (a * b + a * a) * (1 * 1 + 0 * 1))%nat occurrence 4: transitivity through (a * a + c + a * b * (1 * 1 + 0 * 1))%nat occurrence 5: transitivity through (a * b + (a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 6: transitivity through (a * b + a * a + c * (1 * 1 + 0 * 1))%nat occurrence 7: transitivity through (a * a + (a * b + c) * (1 * 1 + 0 * 1))%nat File "./theories/Caveats.v", line 366, characters 2-20: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((a * b + a * a + c) * 1)%nat occurrence 1: transitivity through (a * b + c + a * a * 1)%nat occurrence 2: transitivity through (c + (a * b + a * a) * 1)%nat occurrence 3: transitivity through (a * a + c + a * b * 1)%nat occurrence 4: transitivity through (a * b + (a * a + c) * 1)%nat occurrence 5: transitivity through (a * b + a * a + c * 1)%nat occurrence 6: transitivity through (a * a + (a * b + c) * 1)%nat /usr/bin/make --no-print-directory -f "Makefile.coq" post-all make[3]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' /usr/bin/make all "OPT:=-byte" -f "Makefile.coq" make[3]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' /usr/bin/make --no-print-directory -f "Makefile.coq" pre-all if [ "8.15.1" != "8.15.1" ]; then\ echo "W: This Makefile was generated by Coq 8.15.1";\ echo "W: while the current Coq version is 8.15.1";\ fi /usr/bin/make --no-print-directory -f "Makefile.coq" real-all "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/coq.ml "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/helper.ml "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/search_monad.ml "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/matcher.ml File "src/matcher.ml", line 191, characters 26-44: 191 | let nf_term_compare = Pervasives.compare ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/theory.ml File "src/theory.ml", line 892, characters 24-42: 892 | cap t (List.sort (Pervasives.compare) indices) ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/print.ml File "src/print.ml", line 83, characters 42-60: 83 | let l = List.sort (fun (n,_) (n',_) -> Pervasives.compare n n') l in ^^^^^^^^^^^^^^^^^^ Alert deprecated: module Stdlib.Pervasives Use Stdlib instead. If you need to stay compatible with OCaml < 4.07, you can use the stdlib-shims library: https://github.com/ocaml/stdlib-shims "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/aac_rewrite.ml "/usr/bin/ocamlfind" ocamlc -c -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 src/aac.ml "/usr/bin/ocamlfind" ocamlc -linkpkg -dontlink str,unix,dynlink,threads,zarith -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -pack -o src/aac_plugin.cmo src/coq.cmo src/helper.cmo src/search_monad.cmo src/matcher.cmo src/theory.cmo src/print.cmo src/aac_rewrite.cmo src/aac.cmo "/usr/bin/ocamlfind" ocamlc -linkpkg -dontlink str,unix,dynlink,threads,zarith -thread -rectypes -w -a+1..3-4+5..8-9+10..26-27+28..40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70 -safe-string -strict-sequence -I src -I "/usr/lib/ocaml/coq/../coq-core//boot" -I "/usr/lib/ocaml/coq/../coq-core//config" -I "/usr/lib/ocaml/coq/../coq-core//lib" -I "/usr/lib/ocaml/coq/../coq-core//clib" -I "/usr/lib/ocaml/coq/../coq-core//kernel" -I "/usr/lib/ocaml/coq/../coq-core//library" -I "/usr/lib/ocaml/coq/../coq-core//engine" -I "/usr/lib/ocaml/coq/../coq-core//pretyping" -I "/usr/lib/ocaml/coq/../coq-core//interp" -I "/usr/lib/ocaml/coq/../coq-core//gramlib" -I "/usr/lib/ocaml/coq/../coq-core//parsing" -I "/usr/lib/ocaml/coq/../coq-core//proofs" -I "/usr/lib/ocaml/coq/../coq-core//tactics" -I "/usr/lib/ocaml/coq/../coq-core//toplevel" -I "/usr/lib/ocaml/coq/../coq-core//printing" -I "/usr/lib/ocaml/coq/../coq-core//ide" -I "/usr/lib/ocaml/coq/../coq-core//stm" -I "/usr/lib/ocaml/coq/../coq-core//vernac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/btauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/cc" -I "/usr/lib/ocaml/coq/../coq-core//plugins/derive" -I "/usr/lib/ocaml/coq/../coq-core//plugins/extraction" -I "/usr/lib/ocaml/coq/../coq-core//plugins/firstorder" -I "/usr/lib/ocaml/coq/../coq-core//plugins/funind" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ltac2" -I "/usr/lib/ocaml/coq/../coq-core//plugins/micromega" -I "/usr/lib/ocaml/coq/../coq-core//plugins/nsatz" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ring" -I "/usr/lib/ocaml/coq/../coq-core//plugins/rtauto" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssr" -I "/usr/lib/ocaml/coq/../coq-core//plugins/ssrmatching" -I "/usr/lib/ocaml/coq/../coq-core//plugins/syntax" -warn-error +a-3 -a -o src/aac_plugin.cma src/aac_plugin.cmo "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/AAC.v "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Instances.v "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Tutorial.v All solutions: occurrence 0: transitivity through forall x : X, plus x x 1 possible(s) substitution(s) 0: [x: f (a + a); ] occurrence 1: transitivity through forall x : X, plus (f (x + x)) (f (a + a)) 1 possible(s) substitution(s) 0: [x: a; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 4 possible(s) substitution(s) 0: [x: c; y: dot (d * c * d) b; ] 1: [x: dot c d; y: dot (c * d) b; ] 2: [x: dot (c * d) c; y: dot d b; ] 3: [x: dot (c * d * c) d; y: b; ] occurrence 1: transitivity through forall x y : X, dot (a * x * y * b) b 3 possible(s) substitution(s) 0: [x: c; y: dot (d * c) d; ] 1: [x: dot c d; y: dot c d; ] 2: [x: dot (c * d) c; y: d; ] All solutions: occurrence 0: transitivity through forall x y : X, dot (a * x * y) b 1 possible(s) substitution(s) 0: [x: plus (c * d) (c * d); y: b; ] All solutions: occurrence 0: transitivity through forall x : X, dot (a * x) a 1 possible(s) substitution(s) 0: [x: 1; ] All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: a; y: c; z: dot b c; ] 1: [x: a; y: dot b c; z: c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * c) 2 possible(s) substitution(s) 0: [x: a; y: dot b c; z: b; ] 1: [x: a; y: b; z: dot b c; ] occurrence 2: transitivity through forall x y z : X, plus (x * y + x * z) (a * b * c) 2 possible(s) substitution(s) 0: [x: a; y: c; z: b; ] 1: [x: a; y: b; z: c; ] File "./theories/Tutorial.v", line 232, characters 6-24: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y z : X, plus (x * y) (x * z) 6 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: dot a b; ] 1: [x: a; y: plus (b * c) c; z: b; ] 2: [x: 1; y: 0; z: plus (a * (b * c + c)) (a * b); ] 3: [x: 1; y: plus (a * (b * c + c)) (a * b); z: 0; ] 4: [x: 1; y: dot a b; z: dot a (b * c + c); ] 5: [x: a; y: b; z: plus (b * c) c; ] occurrence 1: transitivity through forall x y z : X, plus (x * y + x * z) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot a (b * c + c); z: 0; ] 1: [x: 1; y: 0; z: dot a (b * c + c); ] occurrence 2: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * b) 4 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: c; ] 1: [x: 1; y: 0; z: plus (b * c) c; ] 2: [x: 1; y: plus (b * c) c; z: 0; ] 3: [x: 1; y: c; z: dot b c; ] occurrence 3: transitivity through forall x y z : X, plus (a * (x * y + x * z + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: dot b c; z: 0; ] 1: [x: 1; y: 0; z: dot b c; ] occurrence 4: transitivity through forall x y z : X, plus (x * y + x * z) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: dot a b; z: 0; ] 1: [x: 1; y: 0; z: dot a b; ] occurrence 5: transitivity through forall x y z : X, plus (a * (b * (x * y + x * z) + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 6: transitivity through forall x y z : X, plus (a * ((x * y + x * z) * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 7: transitivity through forall x y z : X, plus (a * (x * y + x * z + b * c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: c; z: 0; ] 1: [x: 1; y: 0; z: c; ] occurrence 8: transitivity through forall x y z : X, plus ((x * y + x * z) * (b * c + c)) (a * b) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 9: transitivity through forall x y z : X, plus (a * (x * y + x * z)) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: b; z: 0; ] 1: [x: 1; y: 0; z: b; ] occurrence 10: transitivity through forall x y z : X, plus ((x * y + x * z) * b) (a * (b * c + c)) 2 possible(s) substitution(s) 0: [x: 1; y: a; z: 0; ] 1: [x: 1; y: 0; z: a; ] occurrence 11: transitivity through plus (a * (b * c + c)) ((1 * 1 + 1 * 0) * (a * b)) occurrence 12: transitivity through plus (a * (b * c + c)) (a * b * (1 * 1 + 1 * 0)) occurrence 13: transitivity through plus (a * (b * c + c)) (a * ((1 * 1 + 1 * 0) * b)) occurrence 14: transitivity through plus (a * b) ((1 * 1 + 1 * 0) * (a * (b * c + c))) occurrence 15: transitivity through plus (a * b) (a * (b * c + c) * (1 * 1 + 1 * 0)) occurrence 16: transitivity through plus (a * b) (a * (b * c + (1 * 1 + 1 * 0) * c)) occurrence 17: transitivity through plus (a * b) (a * (b * c + c * (1 * 1 + 1 * 0))) occurrence 18: transitivity through plus (a * b) (a * (c + (1 * 1 + 1 * 0) * (b * c))) occurrence 19: transitivity through plus (a * b) (a * (c + b * c * (1 * 1 + 1 * 0))) occurrence 20: transitivity through plus (a * b) (a * (c + b * ((1 * 1 + 1 * 0) * c))) occurrence 21: transitivity through plus (a * b) (a * ((1 * 1 + 1 * 0) * (b * c + c))) occurrence 22: transitivity through dot (a * (b * c + c) + a * b) (1 * 1 + 1 * 0) occurrence 23: transitivity through dot (1 * 1 + 1 * 0) (a * (b * c + c) + a * b) occurrence 24: transitivity through plus (a * (b * c + c)) ((1 * 0 + 1 * 1) * (a * b)) occurrence 25: transitivity through plus (a * (b * c + c)) (a * b * (1 * 0 + 1 * 1)) occurrence 26: transitivity through plus (a * (b * c + c)) (a * ((1 * 0 + 1 * 1) * b)) occurrence 27: transitivity through plus (a * b) ((1 * 0 + 1 * 1) * (a * (b * c + c))) occurrence 28: transitivity through plus (a * b) (a * (b * c + c) * (1 * 0 + 1 * 1)) occurrence 29: transitivity through plus (a * b) (a * (b * c + (1 * 0 + 1 * 1) * c)) occurrence 30: transitivity through plus (a * b) (a * (b * c + c * (1 * 0 + 1 * 1))) occurrence 31: transitivity through plus (a * b) (a * (c + (1 * 0 + 1 * 1) * (b * c))) occurrence 32: transitivity through plus (a * b) (a * (c + b * c * (1 * 0 + 1 * 1))) occurrence 33: transitivity through plus (a * b) (a * (c + b * ((1 * 0 + 1 * 1) * c))) occurrence 34: transitivity through plus (a * b) (a * ((1 * 0 + 1 * 1) * (b * c + c))) occurrence 35: transitivity through dot (a * (b * c + c) + a * b) (1 * 0 + 1 * 1) occurrence 36: transitivity through dot (1 * 0 + 1 * 1) (a * (b * c + c) + a * b) occurrence 37: transitivity through plus (a * (b * c + c) + a * b) (1 * 0 + 1 * 0) occurrence 38: transitivity through plus (a * (b * c + c)) (a * (b + (1 * 0 + 1 * 0))) occurrence 39: transitivity through plus (a * (b * c + c)) ((a + (1 * 0 + 1 * 0)) * b) occurrence 40: transitivity through plus (a * b) (a * (b * c + c + (1 * 0 + 1 * 0))) occurrence 41: transitivity through plus (a * b) (a * (c + b * (c + (1 * 0 + 1 * 0)))) occurrence 42: transitivity through plus (a * b) (a * (c + (b + (1 * 0 + 1 * 0)) * c)) occurrence 43: transitivity through plus (a * b) ((a + (1 * 0 + 1 * 0)) * (b * c + c)) occurrence 44: transitivity through plus (a * (b * c + c) + a * b) (0 * 1 + 0 * 1) occurrence 45: transitivity through plus (a * (b * c + c)) (a * (b + (0 * 1 + 0 * 1))) occurrence 46: transitivity through plus (a * (b * c + c)) ((a + (0 * 1 + 0 * 1)) * b) occurrence 47: transitivity through plus (a * b) (a * (b * c + c + (0 * 1 + 0 * 1))) occurrence 48: transitivity through plus (a * b) (a * (c + b * (c + (0 * 1 + 0 * 1)))) occurrence 49: transitivity through plus (a * b) (a * (c + (b + (0 * 1 + 0 * 1)) * c)) occurrence 50: transitivity through plus (a * b) ((a + (0 * 1 + 0 * 1)) * (b * c + c)) occurrence 51: transitivity through plus (a * (b * c + c)) (a * b * (1 + (1 * 0 + 1 * 0))) occurrence 52: transitivity through plus (a * (b * c + c)) (a * ((1 + (1 * 0 + 1 * 0)) * b)) occurrence 53: transitivity through plus (a * (b * c + c)) ((1 + (1 * 0 + 1 * 0)) * (a * b)) occurrence 54: transitivity through plus (a * b) (a * (b * c + c) * (1 + (1 * 0 + 1 * 0))) occurrence 55: transitivity through plus (a * b) (a * (c + b * c * (1 + (1 * 0 + 1 * 0)))) occurrence 56: transitivity through plus (a * b) (a * (c + b * ((1 + (1 * 0 + 1 * 0)) * c))) occurrence 57: transitivity through plus (a * b) (a * (c + (1 + (1 * 0 + 1 * 0)) * (b * c))) occurrence 58: transitivity through plus (a * b) (a * ((1 + (1 * 0 + 1 * 0)) * (b * c + c))) occurrence 59: transitivity through plus (a * b) ((1 + (1 * 0 + 1 * 0)) * (a * (b * c + c))) occurrence 60: transitivity through plus (a * (b * c + c)) (a * b * (1 + (0 * 1 + 0 * 1))) occurrence 61: transitivity through plus (a * (b * c + c)) (a * ((1 + (0 * 1 + 0 * 1)) * b)) occurrence 62: transitivity through plus (a * (b * c + c)) ((1 + (0 * 1 + 0 * 1)) * (a * b)) occurrence 63: transitivity through plus (a * b) (a * (b * c + c) * (1 + (0 * 1 + 0 * 1))) occurrence 64: transitivity through plus (a * b) (a * (c + b * c * (1 + (0 * 1 + 0 * 1)))) occurrence 65: transitivity through plus (a * b) (a * (c + b * ((1 + (0 * 1 + 0 * 1)) * c))) occurrence 66: transitivity through plus (a * b) (a * (c + (1 + (0 * 1 + 0 * 1)) * (b * c))) occurrence 67: transitivity through plus (a * b) (a * ((1 + (0 * 1 + 0 * 1)) * (b * c + c))) occurrence 68: transitivity through plus (a * b) ((1 + (0 * 1 + 0 * 1)) * (a * (b * c + c))) All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] All solutions: occurrence 0: transitivity through forall x y z : nat, Nat.max (x + y) (x + z) 2 possible(s) substitution(s) 0: [x: a; y: b; z: c; ] 1: [x: a; y: c; z: b; ] Discriminated database Unfoldable variable definitions: all Unfoldable constant definitions: all except: CRelationClasses.Antisymmetric Antisymmetric Associative CRelationClasses.Asymmetric Asymmetric Commutative Idempotent CRelationClasses.Irreflexive Irreflexive CMorphisms.Normalizes Normalizes CRelationClasses.PartialOrder PartialOrder CMorphisms.Proper Proper CMorphisms.ProperProxy ProperProxy CRelationClasses.Reflexive Reflexive ssrclasses.Reflexive CRelationClasses.Symmetric Symmetric CRelationClasses.Transitive Transitive Unconvertible all Basics.arrow arrows Basics.compose Basics.const Basics.flip CMorphisms.forall_relation forall_relation id iff Basics.impl not pointwise_lifting CMorphisms.pointwise_relation pointwise_relation predicate_equivalence predicate_implication CRelationClasses.relation_equivalence relation_equivalence CMorphisms.respectful respectful CRelationClasses.subrelation subrelation Cut: emp For any goal -> For Symmetric -> exact iff_Symmetric(level 0, pattern Symmetric iff, id 0) simple apply @eq_Symmetric(level 0, pattern Symmetric eq, id 0) simple apply @Equivalence.equiv_symmetric(level 1, pattern Symmetric Equivalence.equiv, id 0) simple apply @Equivalence_Symmetric(level 1, pattern Symmetric ?META257, id 0) (*external*) (class_apply @flip_Symmetric)(level 3, pattern Symmetric (Basics.flip _), id 0) (*external*) (class_apply @complement_Symmetric)(level 3, pattern Symmetric (complement _), id 0) simple apply @PER_Symmetric(level 3, pattern Symmetric ?META239, id 0) simple apply @Equivalence.pointwise_symmetric(level 9, pattern Symmetric (pointwise_relation ?META411 ?META413), id 0) For Antisymmetric -> simple eapply @partial_order_antisym(level 2, pattern Antisymmetric ?META316 ?META317 ?META319, id 0) (*external*) (class_apply @flip_Antisymmetric)(level 3, pattern Antisymmetric _ (Basics.flip _), id 0) For CMorphisms.Normalizes -> (*external*) CMorphisms.normalizes(level 1, pattern CMorphisms.Normalizes _ _ _, id 0) For CMorphisms.ProperProxy -> (*external*) (class_apply @CMorphisms.eq_proper_proxy || class_apply @CMorphisms.reflexive_proper_proxy)(level 1, pattern CMorphisms.ProperProxy _ _, id 0) (*external*) (not_evar R; class_apply @CMorphisms.proper_proper_proxy)(level 2, pattern CMorphisms.ProperProxy ?R _, id 0) For Unconvertible -> (*external*) unconvertible(level 0, pattern Unconvertible _ _ _, id 0) For Associative -> exact aac_Zmax_Assoc(level 0, pattern Associative eq BinIntDef.Z.max, id 0) exact aac_Zmin_Assoc(level 0, pattern Associative eq BinIntDef.Z.min, id 0) exact aac_Zmult_Assoc(level 0, pattern Associative eq BinIntDef.Z.mul, id 0) exact aac_Zplus_Assoc(level 0, pattern Associative eq BinIntDef.Z.add, id 0) For CRelationClasses.Reflexive -> exact CRelationClasses.iffT_Reflexive(level 0, pattern CRelationClasses.Reflexive CRelationClasses.iffT, id 0) exact CRelationClasses.arrow_Reflexive(level 0, pattern CRelationClasses.Reflexive CRelationClasses.arrow, id 0) exact CRelationClasses.iff_Reflexive(level 0, pattern CRelationClasses.Reflexive iff, id 0) exact CRelationClasses.impl_Reflexive(level 0, pattern CRelationClasses.Reflexive Basics.impl, id 0) simple apply @CRelationClasses.eq_Reflexive(level 0, pattern CRelationClasses.Reflexive eq, id 0) simple apply @CMorphisms.reflexive_eq_dom_reflexive(level 1, pattern CRelationClasses.Reflexive (CMorphisms.respectful eq ?META303), id 0) (*external*) ( class_apply @CRelationClasses.irreflexivity)(level 1, pattern CRelationClasses.Reflexive (CRelationClasses.complement _), id 0) simple apply @CRelationClasses.Equivalence_Reflexive(level 1, pattern CRelationClasses.Reflexive ?META203, id 0) simple apply @CRelationClasses.PreOrder_Reflexive(level 2, pattern CRelationClasses.Reflexive ?META161, id 0) (*external*) ( apply CRelationClasses.flip_Reflexive)(level 3, pattern CRelationClasses.Reflexive (CRelationClasses.flip _), id 0) For ssrclasses.Reflexive -> exact ssrclasses.iff_Reflexive(level 0, pattern ssrclasses.Reflexive iff, id 0) simple apply @ssrclasses.eq_Reflexive(level 0, pattern ssrclasses.Reflexive eq, id 0) simple apply @ssrsetoid.compat_Reflexive(level 12, pattern ssrclasses.Reflexive ?META268, id 0) For Commutative -> exact aac_Zmax_Comm(level 0, pattern Commutative eq BinIntDef.Z.max, id 0) exact aac_Zmin_Comm(level 0, pattern Commutative eq BinIntDef.Z.min, id 0) exact aac_Zmult_Comm(level 0, pattern Commutative eq BinIntDef.Z.mul, id 0) exact aac_Zplus_Comm(level 0, pattern Commutative eq BinIntDef.Z.add, id 0) For Reflexive -> exact iff_Reflexive(level 0, pattern Reflexive iff, id 0) exact impl_Reflexive(level 0, pattern Reflexive Basics.impl, id 0) simple apply @eq_Reflexive(level 0, pattern Reflexive eq, id 0) simple apply @Equivalence.equiv_reflexive(level 1, pattern Reflexive Equivalence.equiv, id 0) simple apply @reflexive_eq_dom_reflexive(level 1, pattern Reflexive (respectful eq ?META358), id 0) (*external*) (class_apply @irreflexivity)(level 1, pattern Reflexive (complement _), id 0) simple apply @Equivalence_Reflexive(level 1, pattern Reflexive ?META251, id 0) simple apply @PreOrder_Reflexive(level 2, pattern Reflexive ?META209, id 0) (*external*) (apply flip_Reflexive)(level 3, pattern Reflexive (Basics.flip _), id 0) exact Z.divide_reflexive(level 5, pattern Reflexive Z.divide, id 0) exact N.divide_reflexive(level 5, pattern Reflexive N.divide, id 0) exact Nat.divide_reflexive(level 5, pattern Reflexive Nat.divide, id 0) simple apply @Equivalence.pointwise_reflexive(level 9, pattern Reflexive (pointwise_relation ?META403 ?META405), id 0) For CRelationClasses.Asymmetric -> simple apply @CRelationClasses.StrictOrder_Asymmetric(level 1, pattern CRelationClasses.Asymmetric ?META185, id 0) (*external*) ( class_apply @CRelationClasses.flip_Asymmetric)(level 3, pattern CRelationClasses.Asymmetric (CRelationClasses.flip _), id 0) For CRelationClasses.Irreflexive -> simple apply @CRelationClasses.StrictOrder_Irreflexive(level 1, pattern CRelationClasses.Irreflexive ?META173, id 0) (*external*) ( class_apply @CRelationClasses.flip_Irreflexive)(level 3, pattern CRelationClasses.Irreflexive (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CRelationClasses.complement_Irreflexive)(level 3, pattern CRelationClasses.Irreflexive (CRelationClasses.complement _), id 0) For Proper -> exact Qminmax.Q.min_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qminmax.Qmin, id 0) exact Qminmax.Q.max_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qminmax.Qmax, id 0) exact Qminmax.Q.Proper_instance_0(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qle, id 0) exact Qminmax.Q.OT.lt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) exact QOrderedType.QOrder.TO.lt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) exact QOrderedType.Q_as_OT.lt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) simple apply FMapPositive.PositiveMap.ME.ltk_compat'(level 0, pattern Proper (FMapPositive.PositiveMap.ME.eqke (elt:=?META923) ==> FMapPositive.PositiveMap.ME.eqke (elt:=?META923) ==> iff) (FMapPositive.PositiveMap.ME.ltk (elt:=?META923)), id 0) simple apply FMapPositive.PositiveMap.ME.ltk_compat(level 0, pattern Proper (FMapPositive.PositiveMap.ME.eqk (elt:=?META921) ==> FMapPositive.PositiveMap.ME.eqk (elt:=?META921) ==> iff) (FMapPositive.PositiveMap.ME.ltk (elt:=?META921)), id 0) exact FMapPositive.PositiveMap.ME.MO.lt_compat(level 0, pattern Proper (eq ==> eq ==> iff) OrderedTypeEx.PositiveOrderedTypeBits.bits_lt, id 0) simple apply SetoidList.rev_eqlistA_compat(level 0, pattern Proper (SetoidList.eqlistA ?META812 ==> SetoidList.eqlistA ?META812) (List.rev (A:=?META811)), id 0) simple apply SetoidList.app_eqlistA_compat(level 0, pattern Proper (SetoidList.eqlistA ?META808 ==> SetoidList.eqlistA ?META808 ==> SetoidList.eqlistA ?META808) (app (A:=?META807)), id 0) simple apply Permutation.Permutation_flat_map(level 0, pattern Proper (Permutation.Permutation (A:=?META1109) ==> Permutation.Permutation (A:=?META1110)) (List.flat_map ?META1111), id 0) simple apply Permutation.Permutation_map'(level 0, pattern Proper (Permutation.Permutation (A:=?META1103) ==> Permutation.Permutation (A:=?META1104)) (List.map ?META1105), id 0) simple apply Permutation.Permutation_NoDup'(level 0, pattern Proper (Permutation.Permutation (A:=?META1101) ==> iff) (List.NoDup (A:=?META1101)), id 0) simple apply Permutation.Permutation_Exists(level 0, pattern Proper (Permutation.Permutation (A:=?META1097) ==> Basics.impl) (List.Exists ?META1098), id 0) simple apply Permutation.Permutation_Forall(level 0, pattern Proper (Permutation.Permutation (A:=?META1093) ==> Basics.impl) (List.Forall ?META1094), id 0) simple apply Permutation.Permutation_rev'(level 0, pattern Proper (Permutation.Permutation (A:=?META1089) ==> Permutation.Permutation (A:=?META1089)) (List.rev (A:=?META1089)), id 0) simple apply Permutation.Permutation_app'(level 0, pattern Proper (Permutation.Permutation (A:=?META1087) ==> Permutation.Permutation (A:=?META1087) ==> Permutation.Permutation (A:=?META1087)) (app (A:=?META1087)), id 0) simple apply Permutation.Permutation_in'(level 0, pattern Proper (respectful eq (Permutation.Permutation (A:=?META1085) ==> iff)) (List.In (A:=?META1085)), id 0) simple apply Permutation.Permutation_cons(level 0, pattern Proper (respectful eq (Permutation.Permutation (A:=?META1083) ==> Permutation.Permutation (A:=?META1083))) cons, id 0) exact Qreduction.Qminus'_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qminus', id 0) exact Qreduction.Qmult'_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qmult', id 0) exact Qreduction.Qplus'_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qplus', id 0) exact Qreduction.Qred_comp_Proper(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq) Qreduction.Qred, id 0) exact QArith_base.Qpower_comp(level 0, pattern Proper (QArith_base.Qeq ==> eq ==> QArith_base.Qeq) QArith_base.Qpower, id 0) exact QArith_base.Qpower_positive_comp(level 0, pattern Proper (QArith_base.Qeq ==> eq ==> QArith_base.Qeq) QArith_base.Qpower_positive, id 0) exact QArith_base.Qleb_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> eq) QArith_base.Qle_bool, id 0) exact QArith_base.Qeqb_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> eq) QArith_base.Qeq_bool, id 0) exact QArith_base.Qlt_compat(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qlt, id 0) exact QArith_base.Qle_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> iff) QArith_base.Qle, id 0) exact QArith_base.Qcompare_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> eq) QArith_base.Qcompare, id 0) exact QArith_base.Qdiv_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qdiv, id 0) exact QArith_base.Qinv_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qinv, id 0) exact QArith_base.Qmult_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qmult, id 0) exact QArith_base.Qminus_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qminus, id 0) exact QArith_base.Qopp_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qopp, id 0) exact QArith_base.Qplus_comp(level 0, pattern Proper (QArith_base.Qeq ==> QArith_base.Qeq ==> QArith_base.Qeq) QArith_base.Qplus, id 0) exact Z.ones_wd(level 0, pattern Proper (eq ==> eq) Z.ones, id 0) exact Z.lnot_wd(level 0, pattern Proper (eq ==> eq) Z.lnot, id 0) exact Z.clearbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.clearbit, id 0) exact Z.setbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.setbit, id 0) exact Z.ldiff_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.ldiff, id 0) exact Z.lor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.lor, id 0) exact Z.land_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.land, id 0) exact Z.lxor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.lxor, id 0) exact Z.div2_wd(level 0, pattern Proper (eq ==> eq) Z.div2, id 0) exact Z.shiftl_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.shiftl, id 0) exact Z.shiftr_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.shiftr, id 0) exact Z.testbit_eqf(level 0, pattern Proper (eq ==> Z.eqf) Z.testbit, id 0) exact Z.b2z_wd(level 0, pattern Proper (eq ==> eq) Z.b2z, id 0) exact Z.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) Z.eqb, id 0) exact Z.lcm_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.lcm, id 0) exact Z.Bezout_wd(level 0, pattern Proper (eq ==> eq ==> eq ==> iff) Z.Bezout, id 0) exact Z.gcd_wd(level 0, pattern Proper (eq ==> eq ==> eq) Z.gcd, id 0) exact Z.divide_wd(level 0, pattern Proper (eq ==> eq ==> iff) Z.divide, id 0) exact Z.log2_up_wd(level 0, pattern Proper (eq ==> eq) Z.log2_up, id 0) exact Z.log2_wd(level 0, pattern Proper (eq ==> eq) Z.log2, id 0) exact Z.sqrt_up_wd(level 0, pattern Proper (eq ==> eq) Z.sqrt_up, id 0) exact Z.sqrt_wd(level 0, pattern Proper (eq ==> eq) Z.sqrt, id 0) exact Z.odd_wd(level 0, pattern Proper (eq ==> eq) Z.odd, id 0) exact Z.even_wd(level 0, pattern Proper (eq ==> eq) Z.even, id 0) exact Z.Odd_wd(level 0, pattern Proper (eq ==> iff) Z.Odd, id 0) exact Z.Even_wd(level 0, pattern Proper (eq ==> iff) Z.Even, id 0) exact Z.sgn_wd(level 0, pattern Proper (eq ==> eq) Z.sgn, id 0) exact Z.abs_wd(level 0, pattern Proper (eq ==> eq) Z.abs, id 0) exact Z.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) Z.min, id 0) exact Z.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) Z.max, id 0) exact Z.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) Z.le, id 0) exact Z.le_wd(level 0, pattern Proper (eq ==> eq ==> iff) Z.le, id 0) exact N.lnot_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lnot, id 0) exact N.ones_wd(level 0, pattern Proper (eq ==> eq) N.ones, id 0) exact N.clearbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.clearbit, id 0) exact N.setbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.setbit, id 0) exact N.ldiff_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.ldiff, id 0) exact N.lor_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lor, id 0) exact N.land_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.land, id 0) exact N.lxor_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lxor, id 0) exact N.div2_wd(level 0, pattern Proper (eq ==> eq) N.div2, id 0) exact N.shiftl_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.shiftl, id 0) exact N.shiftr_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.shiftr, id 0) exact N.testbit_eqf(level 0, pattern Proper (eq ==> N.eqf) N.testbit, id 0) exact N.b2n_proper(level 0, pattern Proper (eq ==> eq) N.b2n, id 0) exact N.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) N.eqb, id 0) exact N.lcm_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.lcm, id 0) exact N.Bezout_wd(level 0, pattern Proper (eq ==> eq ==> eq ==> iff) N.Bezout, id 0) exact N.gcd_wd(level 0, pattern Proper (eq ==> eq ==> eq) N.gcd, id 0) exact N.divide_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.divide, id 0) exact N.log2_up_wd(level 0, pattern Proper (eq ==> eq) N.log2_up, id 0) exact N.log2_wd(level 0, pattern Proper (eq ==> eq) N.log2, id 0) exact N.sqrt_up_wd(level 0, pattern Proper (eq ==> eq) N.sqrt_up, id 0) exact N.Private_NZSqrt.sqrt_wd(level 0, pattern Proper (eq ==> eq) N.sqrt, id 0) exact N.odd_wd(level 0, pattern Proper (eq ==> eq) N.odd, id 0) exact N.even_wd(level 0, pattern Proper (eq ==> eq) N.even, id 0) exact N.Odd_wd(level 0, pattern Proper (eq ==> iff) N.Odd, id 0) exact N.Even_wd(level 0, pattern Proper (eq ==> iff) N.Even, id 0) exact N.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) N.min, id 0) exact N.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) N.max, id 0) exact N.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) N.le, id 0) exact N.lt_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.lt_alt, id 0) exact N.le_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.le_alt, id 0) exact N.le_wd(level 0, pattern Proper (eq ==> eq ==> iff) N.le, id 0) simple apply @N.recursion_wd(level 0, pattern Proper (respectful ?META763 ((eq ==> respectful ?META763 ?META763) ==> respectful eq ?META763)) N.recursion, id 0) exact Pos.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) Pos.min, id 0) exact Pos.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) Pos.max, id 0) exact Pos.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) Pos.le, id 0) exact Pos.lt_compat(level 0, pattern Proper (eq ==> eq ==> iff) Pos.lt, id 0) exact Pos.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) Pos.eqb, id 0) exact Nat.lnot_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lnot, id 0) exact Nat.ones_wd(level 0, pattern Proper (eq ==> eq) Nat.ones, id 0) exact Nat.clearbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.clearbit, id 0) exact Nat.setbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.setbit, id 0) exact Nat.ldiff_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.ldiff, id 0) exact Nat.lor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lor, id 0) exact Nat.land_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.land, id 0) exact Nat.lxor_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lxor, id 0) exact Nat.div2_wd(level 0, pattern Proper (eq ==> eq) Nat.div2, id 0) exact Nat.shiftl_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.shiftl, id 0) exact Nat.shiftr_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.shiftr, id 0) exact Nat.testbit_eqf(level 0, pattern Proper (eq ==> Nat.eqf) Nat.testbit, id 0) exact Nat.b2n_proper(level 0, pattern Proper (eq ==> eq) Nat.b2n, id 0) exact Nat.eqb_compat(level 0, pattern Proper (eq ==> eq ==> eq) Nat.eqb, id 0) exact Nat.lcm_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.lcm, id 0) exact Nat.Bezout_wd(level 0, pattern Proper (eq ==> eq ==> eq ==> iff) Nat.Bezout, id 0) exact Nat.gcd_wd(level 0, pattern Proper (eq ==> eq ==> eq) Nat.gcd, id 0) exact Nat.divide_wd(level 0, pattern Proper (eq ==> eq ==> iff) Nat.divide, id 0) exact Nat.log2_up_wd(level 0, pattern Proper (eq ==> eq) Nat.log2_up, id 0) exact Nat.log2_wd(level 0, pattern Proper (eq ==> eq) Nat.log2, id 0) exact Nat.sqrt_up_wd(level 0, pattern Proper (eq ==> eq) Nat.sqrt_up, id 0) exact Nat.Private_NZSqrt.sqrt_wd(level 0, pattern Proper (eq ==> eq) Nat.sqrt, id 0) exact Nat.odd_wd(level 0, pattern Proper (eq ==> eq) Nat.odd, id 0) exact Nat.even_wd(level 0, pattern Proper (eq ==> eq) Nat.even, id 0) exact Nat.Odd_wd(level 0, pattern Proper (eq ==> iff) Nat.Odd, id 0) exact Nat.Even_wd(level 0, pattern Proper (eq ==> iff) Nat.Even, id 0) exact Nat.min_compat(level 0, pattern Proper (eq ==> eq ==> eq) Nat.min, id 0) exact Nat.max_compat(level 0, pattern Proper (eq ==> eq ==> eq) Nat.max, id 0) exact Nat.Proper_instance_0(level 0, pattern Proper (eq ==> eq ==> iff) le, id 0) exact Nat.lt_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) Nat.lt_alt, id 0) exact Nat.le_alt_wd(level 0, pattern Proper (eq ==> eq ==> iff) Nat.le_alt, id 0) exact Nat.le_wd(level 0, pattern Proper (eq ==> eq ==> iff) le, id 0) simple apply @Nat.recursion_wd(level 0, pattern Proper (respectful ?META686 ((eq ==> respectful ?META686 ?META686) ==> respectful eq ?META686)) Nat.recursion, id 0) exact Nat.testbit_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.testbit, id 0) exact Nat.lt_wd(level 0, pattern Proper (eq ==> eq ==> iff) lt, id 0) exact Nat.mod_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.modulo, id 0) exact Nat.div_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.div, id 0) exact Nat.pow_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.pow, id 0) exact Nat.mul_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.mul, id 0) exact Nat.sub_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.sub, id 0) exact Nat.add_wd(level 0, pattern Proper (eq ==> eq ==> eq) Init.Nat.add, id 0) exact Nat.pred_wd(level 0, pattern Proper (eq ==> eq) Init.Nat.pred, id 0) exact Nat.succ_wd(level 0, pattern Proper (eq ==> eq) S, id 0) simple apply @Morphisms_Prop.well_founded_morphism(level 0, pattern Proper (relation_equivalence ==> iff) (well_founded (A:=?META733)), id 0) simple apply @Morphisms_Prop.Acc_rel_morphism(level 0, pattern Proper (relation_equivalence ==> respectful eq iff) (Acc (A:=?META731)), id 0) simple apply @Morphisms_Prop.all_iff_morphism(level 0, pattern Proper (pointwise_relation ?META691 iff ==> iff) (all (A:=?META691)), id 0) simple apply @Morphisms_Prop.ex_iff_morphism(level 0, pattern Proper (pointwise_relation ?META559 iff ==> iff) (ex (A:=?META559)), id 0) exact Morphisms_Prop.iff_iff_iff_impl_morphism(level 0, pattern Proper (iff ==> iff ==> iff) Basics.impl, id 0) exact Morphisms_Prop.or_iff_morphism(level 0, pattern Proper (iff ==> iff ==> iff) or, id 0) exact Morphisms_Prop.and_iff_morphism(level 0, pattern Proper (iff ==> iff ==> iff) and, id 0) exact Morphisms_Prop.not_iff_morphism(level 0, pattern Proper (iff ==> iff) not, id 0) simple apply @proper_proper(level 0, pattern Proper (relation_equivalence ==> respectful eq iff) Proper, id 0) simple apply @respectful_morphism(level 0, pattern Proper (relation_equivalence ==> relation_equivalence ==> relation_equivalence) respectful, id 0) simple apply @compose_proper(level 0, pattern Proper (respectful ?META348 ?META349 ==> respectful ?META347 ?META348 ==> respectful ?META347 ?META349) Basics.compose, id 0) simple apply @proper_subrelation_proper(level 0, pattern Proper (subrelation ==> respectful eq Basics.impl) Proper, id 0) simple apply SetoidList.equivlistA_app_proper(level 1, pattern Proper (SetoidList.equivlistA ?META792 ==> SetoidList.equivlistA ?META792 ==> SetoidList.equivlistA ?META792) (app (A:=?META791)), id 0) simple apply SetoidList.equivlistA_cons_proper(level 1, pattern Proper (respectful ?META786 (SetoidList.equivlistA ?META786 ==> SetoidList.equivlistA ?META786)) cons, id 0) simple apply SetoidList.InA_compat(level 1, pattern Proper (respectful ?META780 (SetoidList.equivlistA ?META780 ==> iff)) (SetoidList.InA ?META780), id 0) simple apply @Morphisms_Prop.all_flip_impl_morphism(level 1, pattern Proper (pointwise_relation ?META719 (Basics.flip Basics.impl) ==> Basics.flip Basics.impl) (all (A:=?META719)), id 0) simple apply @Morphisms_Prop.all_impl_morphism(level 1, pattern Proper (pointwise_relation ?META705 Basics.impl ==> Basics.impl) (all (A:=?META705)), id 0) simple apply @Morphisms_Prop.ex_flip_impl_morphism(level 1, pattern Proper (pointwise_relation ?META635 (Basics.flip Basics.impl) ==> Basics.flip Basics.impl) (ex (A:=?META635)), id 0) simple apply @Morphisms_Prop.ex_impl_morphism(level 1, pattern Proper (pointwise_relation ?META597 Basics.impl ==> Basics.impl) (ex (A:=?META597)), id 0) exact Morphisms_Prop.or_impl_morphism(level 1, pattern Proper (Basics.impl ==> Basics.impl ==> Basics.impl) or, id 0) exact Morphisms_Prop.and_impl_morphism(level 1, pattern Proper (Basics.impl ==> Basics.impl ==> Basics.impl) and, id 0) exact Morphisms_Prop.not_impl_morphism(level 1, pattern Proper (Basics.impl --> Basics.impl) not, id 0) (*external*) (apply @flip_proper)(level 1, pattern Proper _ (Basics.flip _), id 0) (*external*) (apply @complement_proper)(level 1, pattern Proper _ (complement _), id 0) simple apply @PER_morphism(level 1, pattern Proper (respectful ?META339 (respectful ?META339 iff)) ?META339, id 0) simple apply @trans_contra_co_morphism(level 1, pattern Proper (respectful (Basics.flip ?META287) (respectful ?META287 Basics.impl)) ?META287, id 0) simple apply @subrelation_id_proper(level 1, pattern Proper (respectful ?META267 ?META268) id, id 0) simple apply SetoidList.InfA_compat(level 2, pattern Proper (respectful ?META798 (SetoidList.eqlistA ?META798 ==> iff)) (Sorted.HdRel ?META800), id 0) simple apply @Morphisms_Prop.Acc_pt_morphism(level 2, pattern Proper (respectful ?META722 iff) (Acc ?META723), id 0) (*external*) (class_apply @proper_flip_proper)(level 2, pattern Proper (Basics.flip _) _, id 0) simple apply @trans_co_eq_inv_impl_morphism(level 2, pattern Proper (respectful ?META333 (respectful eq (Basics.flip Basics.impl))) ?META333, id 0) simple apply @per_partial_app_morphism(level 2, pattern Proper (respectful ?META325 iff) (?META325 ?META327), id 0) simple eapply @PartialOrder_proper(level 3, pattern Proper (respectful ?META371 (respectful ?META371 iff)) ?META373, id 0) simple apply @trans_sym_contra_impl_morphism(level 3, pattern Proper (respectful (Basics.flip ?META317) Basics.impl) (?META317 ?META319), id 0) simple apply @trans_sym_co_inv_impl_morphism(level 3, pattern Proper (respectful ?META309 (Basics.flip Basics.impl)) (?META309 ?META311), id 0) simple apply @trans_co_impl_morphism(level 3, pattern Proper (respectful ?META301 Basics.impl) (?META301 ?META303), id 0) simple apply @trans_contra_inv_impl_morphism(level 3, pattern Proper (respectful (Basics.flip ?META293) (Basics.flip Basics.impl)) (?META293 ?META295), id 0) (*external*) partial_application_tactic(level 4, pattern Proper _ _, id 0) (*external*) proper_subrelation(level 5, pattern Proper ?H _, id 0) (*external*) proper_normalization(level 6, pattern Proper _ _, id 0) (*external*) proper_reflexive(level 7, pattern Proper _ _, id 0) exact Permutation.Permutation_list_max(level 10, pattern Proper (Permutation.Permutation (A:=nat) ==> eq) List.list_max, id 0) exact Permutation.Permutation_list_sum(level 10, pattern Proper (Permutation.Permutation (A:=nat) ==> eq) List.list_sum, id 0) simple apply Permutation.Permutation_length'(level 10, pattern Proper (Permutation.Permutation (A:=?META1091) ==> eq) (length (A:=?META1091)), id 0) For Asymmetric -> simple apply @StrictOrder_Asymmetric(level 1, pattern Asymmetric ?META233, id 0) (*external*) (class_apply @flip_Asymmetric)(level 3, pattern Asymmetric (Basics.flip _), id 0) For Irreflexive -> simple apply @StrictOrder_Irreflexive(level 1, pattern Irreflexive ?META221, id 0) (*external*) (class_apply @flip_Irreflexive)(level 3, pattern Irreflexive (Basics.flip _), id 0) (*external*) (class_apply @complement_Irreflexive)(level 3, pattern Irreflexive (complement _), id 0) For CRelationClasses.Transitive -> exact CRelationClasses.iffT_Transitive(level 0, pattern CRelationClasses.Transitive CRelationClasses.iffT, id 0) exact CRelationClasses.arrow_Transitive(level 0, pattern CRelationClasses.Transitive CRelationClasses.arrow, id 0) exact CRelationClasses.iff_Transitive(level 0, pattern CRelationClasses.Transitive iff, id 0) exact CRelationClasses.impl_Transitive(level 0, pattern CRelationClasses.Transitive Basics.impl, id 0) simple apply @CRelationClasses.eq_Transitive(level 0, pattern CRelationClasses.Transitive eq, id 0) simple apply @CRelationClasses.Equivalence_Transitive(level 1, pattern CRelationClasses.Transitive ?META215, id 0) simple apply @CRelationClasses.StrictOrder_Transitive(level 1, pattern CRelationClasses.Transitive ?META179, id 0) simple apply @CRelationClasses.PreOrder_Transitive(level 2, pattern CRelationClasses.Transitive ?META167, id 0) (*external*) ( class_apply @CRelationClasses.flip_Transitive)(level 3, pattern CRelationClasses.Transitive (CRelationClasses.flip _), id 0) simple apply @CRelationClasses.PER_Transitive(level 3, pattern CRelationClasses.Transitive ?META197, id 0) For CMorphisms.Proper -> simple apply @CMorphisms.proper_proper(level 0, pattern CMorphisms.Proper (CMorphisms.respectful CRelationClasses.relation_equivalence (CMorphisms.respectful eq CRelationClasses.iffT)) CMorphisms.Proper, id 0) simple apply @CMorphisms.respectful_morphism(level 0, pattern CMorphisms.Proper (CMorphisms.respectful CRelationClasses.relation_equivalence (CMorphisms.respectful CRelationClasses.relation_equivalence CRelationClasses.relation_equivalence)) CMorphisms.respectful, id 0) simple apply CMorphisms.compose_proper(level 0, pattern CMorphisms.Proper (CMorphisms.respectful (CMorphisms.respectful ?META294 ?META295) (CMorphisms.respectful (CMorphisms.respectful ?META293 ?META294) (CMorphisms.respectful ?META293 ?META295))) Basics.compose, id 0) simple apply @CMorphisms.proper_subrelation_proper_arrow(level 0, pattern CMorphisms.Proper (CMorphisms.respectful CRelationClasses.subrelation (CMorphisms.respectful eq CRelationClasses.arrow)) CMorphisms.Proper, id 0) (*external*) (apply @CMorphisms.flip_proper)(level 1, pattern CMorphisms.Proper _ (CRelationClasses.flip _), id 0) simple apply @CMorphisms.PER_type_morphism(level 1, pattern CMorphisms.Proper (CMorphisms.respectful ?META285 (CMorphisms.respectful ?META285 CRelationClasses.iffT)) ?META285, id 0) simple apply @CMorphisms.trans_contra_co_type_morphism(level 1, pattern CMorphisms.Proper (CMorphisms.respectful (CRelationClasses.flip ?META233) (CMorphisms.respectful ?META233 CRelationClasses.arrow)) ?META233, id 0) simple apply @CMorphisms.subrelation_id_proper(level 1, pattern CMorphisms.Proper (CMorphisms.respectful ?META213 ?META214) id, id 0) (*external*) (class_apply @CMorphisms.proper_flip_proper)(level 2, pattern CMorphisms.Proper (CRelationClasses.flip _) _, id 0) simple apply @CMorphisms.trans_co_eq_inv_arrow_morphism(level 2, pattern CMorphisms.Proper (CMorphisms.respectful ?META279 (CMorphisms.respectful eq (CRelationClasses.flip CRelationClasses.arrow))) ?META279, id 0) simple apply @CMorphisms.per_partial_app_type_morphism(level 2, pattern CMorphisms.Proper (CMorphisms.respectful ?META271 CRelationClasses.iffT) (?META271 ?META273), id 0) simple eapply @CMorphisms.PartialOrder_proper_type(level 3, pattern CMorphisms.Proper (CMorphisms.respectful ?META365 (CMorphisms.respectful ?META365 CRelationClasses.iffT)) ?META367, id 0) simple apply @CMorphisms.trans_sym_contra_arrow_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful (CRelationClasses.flip ?META263) CRelationClasses.arrow) (?META263 ?META265), id 0) simple apply @CMorphisms.trans_sym_co_inv_impl_type_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful ?META255 (CRelationClasses.flip CRelationClasses.arrow)) (?META255 ?META257), id 0) simple apply @CMorphisms.trans_co_impl_type_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful ?META247 CRelationClasses.arrow) (?META247 ?META249), id 0) simple apply @CMorphisms.trans_contra_inv_impl_type_morphism(level 3, pattern CMorphisms.Proper (CMorphisms.respectful (CRelationClasses.flip ?META239) (CRelationClasses.flip CRelationClasses.arrow)) (?META239 ?META241), id 0) (*external*) CMorphisms.partial_application_tactic(level 4, pattern CMorphisms.Proper _ _, id 0) (*external*) CMorphisms.proper_subrelation(level 5, pattern CMorphisms.Proper ?H _, id 0) (*external*) CMorphisms.proper_normalization(level 6, pattern CMorphisms.Proper _ _, id 0) (*external*) CMorphisms.proper_reflexive(level 7, pattern CMorphisms.Proper _ _, id 0) For CRelationClasses.subrelation -> (*external*) ( class_apply @CMorphisms.flip2)(level 1, pattern CRelationClasses.subrelation _ (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CMorphisms.flip1)(level 1, pattern CRelationClasses.subrelation (CRelationClasses.flip _) _, id 0) exact CMorphisms.iffT_flip_arrow_subrelation(level 2, pattern CRelationClasses.subrelation CRelationClasses.iffT (CRelationClasses.flip CRelationClasses.arrow), id 0) exact CMorphisms.iffT_arrow_subrelation(level 2, pattern CRelationClasses.subrelation CRelationClasses.iffT CRelationClasses.arrow, id 0) exact CMorphisms.iff_flip_impl_subrelation(level 2, pattern CRelationClasses.subrelation iff (CRelationClasses.flip Basics.impl), id 0) exact CMorphisms.iff_impl_subrelation(level 2, pattern CRelationClasses.subrelation iff Basics.impl, id 0) (*external*) ( CMorphisms.subrelation_tac T U)(level 3, pattern CRelationClasses.subrelation ?T ?U, id 0) (*external*) ( apply (CMorphisms.forall_subrelation B R S); intro)(level 4, pattern CRelationClasses.subrelation (CMorphisms.forall_relation ?R) (CMorphisms.forall_relation ?S), id 0) simple apply @CMorphisms.pointwise_subrelation(level 4, pattern CRelationClasses.subrelation (CMorphisms.pointwise_relation ?META222 ?META224) (CMorphisms.pointwise_relation ?META222 ?META225), id 0) (*external*) ( class_apply @CRelationClasses.subrelation_symmetric)(level 4, pattern CRelationClasses.subrelation (CRelationClasses.flip _) _, id 0) For Transitive -> exact iff_Transitive(level 0, pattern Transitive iff, id 0) exact impl_Transitive(level 0, pattern Transitive Basics.impl, id 0) simple apply @eq_Transitive(level 0, pattern Transitive eq, id 0) simple apply @Equivalence.equiv_transitive(level 1, pattern Transitive Equivalence.equiv, id 0) simple apply @Equivalence_Transitive(level 1, pattern Transitive ?META263, id 0) simple apply @StrictOrder_Transitive(level 1, pattern Transitive ?META227, id 0) simple apply @PreOrder_Transitive(level 2, pattern Transitive ?META215, id 0) (*external*) (class_apply @flip_Transitive)(level 3, pattern Transitive (Basics.flip _), id 0) simple apply @PER_Transitive(level 3, pattern Transitive ?META245, id 0) exact Z.divide_transitive(level 5, pattern Transitive Z.divide, id 0) exact N.divide_transitive(level 5, pattern Transitive N.divide, id 0) exact Nat.divide_transitive(level 5, pattern Transitive Nat.divide, id 0) simple apply @Equivalence.pointwise_transitive(level 9, pattern Transitive (pointwise_relation ?META419 ?META421), id 0) For CRelationClasses.PartialOrder -> (*external*) ( class_apply @CRelationClasses.PartialOrder_inverse)(level 3, pattern CRelationClasses.PartialOrder (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CMorphisms.StrictOrder_PartialOrder)(level 4, pattern CRelationClasses.PartialOrder _ (CRelationClasses.relation_disjunction _ _), id 0) For subrelation -> simple apply SetoidList.eqlistA_equivlistA(level 1, pattern subrelation (SetoidList.eqlistA ?META774) (SetoidList.equivlistA ?META774), id 0) (*external*) (class_apply @flip2)(level 1, pattern subrelation _ (Basics.flip _), id 0) (*external*) (class_apply @flip1)(level 1, pattern subrelation (Basics.flip _) _, id 0) exact iff_flip_impl_subrelation(level 2, pattern subrelation iff (Basics.flip Basics.impl), id 0) exact iff_impl_subrelation(level 2, pattern subrelation iff Basics.impl, id 0) (*external*) (subrelation_tac T U)(level 3, pattern subrelation ?T ?U, id 0) (*external*) (apply (forall_subrelation B R S); intro)(level 4, pattern subrelation (forall_relation ?R) (forall_relation ?S), id 0) simple apply @pointwise_subrelation(level 4, pattern subrelation (pointwise_relation ?META276 ?META278) (pointwise_relation ?META276 ?META279), id 0) (*external*) (class_apply @subrelation_symmetric)(level 4, pattern subrelation (Basics.flip _) _, id 0) For Normalizes -> (*external*) normalizes(level 1, pattern Normalizes _ _ _, id 0) For Idempotent -> exact aac_Zmax_Idem(level 0, pattern Idempotent eq BinIntDef.Z.max, id 0) exact aac_Zmin_Idem(level 0, pattern Idempotent eq BinIntDef.Z.min, id 0) For ProperProxy -> (*external*) (class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy)(level 1, pattern ProperProxy _ _, id 0) (*external*) (not_evar R; class_apply @proper_proper_proxy)(level 2, pattern ProperProxy ?R _, id 0) For PartialOrder -> exact Z.le_partialorder(level 0, pattern PartialOrder eq Z.le, id 0) exact N.le_partialorder(level 0, pattern PartialOrder eq N.le, id 0) exact Pos.le_partorder(level 0, pattern PartialOrder eq Pos.le, id 0) exact Nat.le_partialorder(level 0, pattern PartialOrder eq le, id 0) simple apply @subrelation_partial_order(level 0, pattern PartialOrder relation_equivalence subrelation, id 0) (*external*) (class_apply @PartialOrder_inverse)(level 3, pattern PartialOrder (Basics.flip _), id 0) (*external*) (class_apply @StrictOrder_PartialOrder)(level 4, pattern PartialOrder _ (relation_disjunction _ _), id 0) For CRelationClasses.Symmetric -> exact CRelationClasses.iffT_Symmetric(level 0, pattern CRelationClasses.Symmetric CRelationClasses.iffT, id 0) exact CRelationClasses.iff_Symmetric(level 0, pattern CRelationClasses.Symmetric iff, id 0) simple apply @CRelationClasses.eq_Symmetric(level 0, pattern CRelationClasses.Symmetric eq, id 0) simple apply @CRelationClasses.Equivalence_Symmetric(level 1, pattern CRelationClasses.Symmetric ?META209, id 0) (*external*) ( class_apply @CRelationClasses.flip_Symmetric)(level 3, pattern CRelationClasses.Symmetric (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CRelationClasses.complement_Symmetric)(level 3, pattern CRelationClasses.Symmetric (CRelationClasses.complement _), id 0) simple apply @CRelationClasses.PER_Symmetric(level 3, pattern CRelationClasses.Symmetric ?META191, id 0) For CRelationClasses.Antisymmetric -> simple eapply @CRelationClasses.partial_order_antisym(level 2, pattern CRelationClasses.Antisymmetric ?META265 ?META267, id 0) (*external*) ( class_apply @CRelationClasses.flip_Antisymmetric)(level 3, pattern CRelationClasses.Antisymmetric (CRelationClasses.flip _), id 0) For ZifyClasses.BinRel -> exact ZifyInst.Op_eqZ(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_Z_le(level 0, pattern ZifyClasses.BinRel Z.le, id 0) exact ZifyInst.Op_Z_gt(level 0, pattern ZifyClasses.BinRel Z.gt, id 0) exact ZifyInst.Op_Z_lt(level 0, pattern ZifyClasses.BinRel Z.lt, id 0) exact ZifyInst.Op_Z_ge(level 0, pattern ZifyClasses.BinRel Z.ge, id 0) exact ZifyInst.Op_eq_N(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_N_le(level 0, pattern ZifyClasses.BinRel N.le, id 0) exact ZifyInst.Op_N_gt(level 0, pattern ZifyClasses.BinRel N.gt, id 0) exact ZifyInst.Op_N_lt(level 0, pattern ZifyClasses.BinRel N.lt, id 0) exact ZifyInst.Op_N_ge(level 0, pattern ZifyClasses.BinRel N.ge, id 0) exact ZifyInst.Op_eq_pos(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_pos_le(level 0, pattern ZifyClasses.BinRel Pos.le, id 0) exact ZifyInst.Op_pos_gt(level 0, pattern ZifyClasses.BinRel Pos.gt, id 0) exact ZifyInst.Op_pos_lt(level 0, pattern ZifyClasses.BinRel Pos.lt, id 0) exact ZifyInst.Op_pos_ge(level 0, pattern ZifyClasses.BinRel Pos.ge, id 0) exact ZifyInst.Op_Nat_eq(level 0, pattern ZifyClasses.BinRel Nat.eq, id 0) exact ZifyInst.Op_eq_nat(level 0, pattern ZifyClasses.BinRel eq, id 0) exact ZifyInst.Op_Nat_le(level 0, pattern ZifyClasses.BinRel Nat.le, id 0) exact ZifyInst.Op_le(level 0, pattern ZifyClasses.BinRel le, id 0) exact ZifyInst.Op_gt(level 0, pattern ZifyClasses.BinRel gt, id 0) exact ZifyInst.Op_Nat_lt(level 0, pattern ZifyClasses.BinRel Nat.lt, id 0) exact ZifyInst.Op_lt(level 0, pattern ZifyClasses.BinRel lt, id 0) exact ZifyInst.Op_ge(level 0, pattern ZifyClasses.BinRel ge, id 0) For SetoidTactics.DefaultRelation -> simple apply @SetoidTactics.equivalence_default(level 4, pattern SetoidTactics.DefaultRelation ?META473, id 0) For ZifyClasses.InjTyp -> exact ZifyInst.Inj_N_Z(level 0, pattern ZifyClasses.InjTyp N Z, id 0) exact ZifyInst.Inj_pos_Z(level 0, pattern ZifyClasses.InjTyp positive Z, id 0) exact ZifyInst.Inj_nat_Z(level 0, pattern ZifyClasses.InjTyp nat Z, id 0) exact ZifyInst.Inj_Z_Z(level 0, pattern ZifyClasses.InjTyp Z Z, id 0) For CRelationClasses.PreOrder -> simple apply @CRelationClasses.relation_implication_preorder(level 0, pattern CRelationClasses.PreOrder CRelationClasses.subrelation, id 0) (*external*) (class_apply @CRelationClasses.flip_PreOrder)(level 3, pattern CRelationClasses.PreOrder (CRelationClasses.flip _), id 0) (*external*) (class_apply @CMorphisms.StrictOrder_PreOrder)(level 4, pattern CRelationClasses.PreOrder (CRelationClasses.relation_disjunction _ _), id 0) For CRelationClasses.Equivalence -> simple apply @CRelationClasses.relation_equivalence_equivalence(level 0, pattern CRelationClasses.Equivalence CRelationClasses.relation_equivalence, id 0) exact CRelationClasses.iff_equivalence(level 0, pattern CRelationClasses.Equivalence iff, id 0) simple apply @CRelationClasses.eq_equivalence(level 10, pattern CRelationClasses.Equivalence eq, id 0) For PreOrder -> exact preorder_Zle(level 0, pattern PreOrder Z.le, id 0) exact Z.le_preorder(level 0, pattern PreOrder Z.le, id 0) exact N.le_preorder(level 0, pattern PreOrder N.le, id 0) exact Pos.le_preorder(level 0, pattern PreOrder Pos.le, id 0) exact Nat.le_preorder(level 0, pattern PreOrder le, id 0) simple apply @relation_implication_preorder(level 0, pattern PreOrder subrelation, id 0) simple apply @predicate_implication_preorder(level 0, pattern PreOrder predicate_implication, id 0) (*external*) (class_apply @flip_PreOrder)(level 3, pattern PreOrder (Basics.flip _), id 0) (*external*) (class_apply @StrictOrder_PreOrder)(level 4, pattern PreOrder (relation_disjunction _ _), id 0) simple apply @Equivalence_PreOrder(level 10, pattern PreOrder ?META275, id 0) For CRelationClasses.PER -> simple apply @CRelationClasses.Equivalence_PER(level 10, pattern CRelationClasses.PER ?META221, id 0) For ZifyClasses.BinOpSpec -> exact ZifyInst.ZminSpec(level 0, pattern ZifyClasses.BinOpSpec BinIntDef.Z.min, id 0) exact ZifyInst.ZmaxSpec(level 0, pattern ZifyClasses.BinOpSpec BinIntDef.Z.max, id 0) For Equivalence -> exact Qminmax.Q.OT.eq_equiv(level 0, pattern Equivalence QArith_base.Qeq, id 0) exact QOrderedType.QOrder.TO.eq_equiv(level 0, pattern Equivalence QArith_base.Qeq, id 0) simple apply FMapPositive.PositiveMap.eqke_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.eq_key_elt (A:=?META1651)), id 0) simple apply FMapPositive.PositiveMap.eqk_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.eq_key (A:=?META1649)), id 0) simple apply FMapPositive.PositiveMap.ME.eqke_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.ME.eqke (elt:=?META917)), id 0) simple apply FMapPositive.PositiveMap.ME.eqk_equiv(level 0, pattern Equivalence (FMapPositive.PositiveMap.ME.eqk (elt:=?META915)), id 0) exact FMapPositive.PositiveMap.ME.MO.eq_equiv(level 0, pattern Equivalence eq, id 0) simple apply Permutation.Permutation_Equivalence(level 0, pattern Equivalence (Permutation.Permutation (A:=?META1081)), id 0) exact QArith_base.Q_Setoid(level 0, pattern Equivalence QArith_base.Qeq, id 0) exact Ndigits.eqf_equiv(level 0, pattern Equivalence Ndigits.eqf, id 0) exact Z.eqf_equiv(level 0, pattern Equivalence Z.eqf, id 0) exact N.eqf_equiv(level 0, pattern Equivalence N.eqf, id 0) exact Nat.eqf_equiv(level 0, pattern Equivalence Nat.eqf, id 0) simple apply @relation_equivalence_equivalence(level 0, pattern Equivalence relation_equivalence, id 0) simple apply @predicate_equivalence_equivalence(level 0, pattern Equivalence predicate_equivalence, id 0) exact iff_equivalence(level 0, pattern Equivalence iff, id 0) simple apply SetoidList.eqlistA_equiv(level 1, pattern Equivalence (SetoidList.eqlistA ?META768), id 0) simple apply SetoidList.equivlist_equiv(level 1, pattern Equivalence (SetoidList.equivlistA ?META762), id 0) simple apply @Equivalence.pointwise_equivalence(level 9, pattern Equivalence (pointwise_relation ?META427 ?META429), id 0) simple apply @eq_equivalence(level 10, pattern Equivalence eq, id 0) simple apply Permutation.Permutation_transp_equiv(level 100, pattern Equivalence (Permutation.Permutation_transp (A:=?META1115)), id 0) For PER -> simple apply @Equivalence_PER(level 10, pattern PER ?META269, id 0) For Unit -> exact aac_zero_Zplus(level 0, pattern Unit eq BinIntDef.Z.add 0, id 0) exact aac_one(level 0, pattern Unit eq BinIntDef.Z.mul 1, id 0) For CRelationClasses.StrictOrder -> (*external*) ( class_apply @CRelationClasses.flip_StrictOrder)(level 3, pattern CRelationClasses.StrictOrder (CRelationClasses.flip _), id 0) (*external*) ( class_apply @CMorphisms.PartialOrder_StrictOrder)(level 4, pattern CRelationClasses.StrictOrder (CRelationClasses.relation_conjunction _ _), id 0) For ZifyClasses.Saturate -> exact ZifyInst.SatPowNonneg(level 0, pattern ZifyClasses.Saturate BinIntDef.Z.pow, id 0) exact ZifyInst.SatPowPos(level 0, pattern ZifyClasses.Saturate BinIntDef.Z.pow, id 0) For AAC_lift -> exact lift_le_eq(level 0, pattern AAC_lift Z.le eq, id 0) simple apply @aac_lift_subrelation(level 3, pattern AAC_lift ?META1678 ?META1679, id 0) simple apply @aac_lift_proper(level 4, pattern AAC_lift ?META1690 ?META1691, id 0) For DeclConstant.GT -> simple apply @DeclConstant.GT_O(level 1, pattern DeclConstant.GT ?META727, id 0) simple apply @DeclConstant.GT_APP1(level 2, pattern DeclConstant.GT (?META734 ?META735), id 0) simple apply @DeclConstant.GT_APP2(level 3, pattern DeclConstant.GT (?META747 ?META748 ?META749), id 0) For CRelationClasses.RewriteRelation -> simple apply @CRelationClasses.RewriteRelation_instance_2(level 0, pattern CRelationClasses.RewriteRelation CRelationClasses.relation_equivalence, id 0) exact CRelationClasses.RewriteRelation_instance_1(level 0, pattern CRelationClasses.RewriteRelation iff, id 0) exact CRelationClasses.RewriteRelation_instance_0(level 0, pattern CRelationClasses.RewriteRelation Basics.impl, id 0) simple apply @CRelationClasses.equivalence_rewrite_crelation(level 1, pattern CRelationClasses.RewriteRelation ?META227, id 0) For StrictOrder -> exact Qminmax.Q.OT.lt_strorder(level 0, pattern StrictOrder QArith_base.Qlt, id 0) exact QOrderedType.QOrder.TO.lt_strorder(level 0, pattern StrictOrder QArith_base.Qlt, id 0) exact QOrderedType.Q_as_OT.lt_strorder(level 0, pattern StrictOrder QArith_base.Qlt, id 0) simple apply FMapPositive.PositiveMap.ltk_strorder(level 0, pattern StrictOrder (FMapPositive.PositiveMap.lt_key (A:=?META1653)), id 0) simple apply FMapPositive.PositiveMap.ME.ltk_strorder(level 0, pattern StrictOrder (FMapPositive.PositiveMap.ME.ltk (elt:=?META919)), id 0) exact FMapPositive.PositiveMap.ME.MO.lt_strorder(level 0, pattern StrictOrder OrderedTypeEx.PositiveOrderedTypeBits.bits_lt, id 0) exact Z.lt_strorder(level 0, pattern StrictOrder Z.lt, id 0) exact N.lt_strorder(level 0, pattern StrictOrder N.lt, id 0) exact Pos.lt_strorder(level 0, pattern StrictOrder Pos.lt, id 0) exact Nat.lt_strorder(level 0, pattern StrictOrder lt, id 0) (*external*) (class_apply @flip_StrictOrder)(level 3, pattern StrictOrder (Basics.flip _), id 0) (*external*) (class_apply @PartialOrder_StrictOrder)(level 4, pattern StrictOrder (relation_conjunction _ _), id 0) For ZifyClasses.UnOpSpec -> exact ZifyInst.ZabsSpec(level 0, pattern ZifyClasses.UnOpSpec BinIntDef.Z.abs, id 0) exact ZifyInst.ZsgnSpec(level 0, pattern ZifyClasses.UnOpSpec BinIntDef.Z.sgn, id 0) For DeclConstant.DeclaredConstant -> exact DeclConstant.DQ(level 0, pattern DeclConstant.DeclaredConstant QArith_base.Qmake, id 0) exact DeclConstant.DZpow(level 0, pattern DeclConstant.DeclaredConstant BinIntDef.Z.pow, id 0) exact DeclConstant.DZpow_pos(level 0, pattern DeclConstant.DeclaredConstant BinIntDef.Z.pow_pos, id 0) exact DeclConstant.DZneg(level 0, pattern DeclConstant.DeclaredConstant (-1), id 0) exact DeclConstant.DZpos(level 0, pattern DeclConstant.DeclaredConstant Z.pos, id 0) exact DeclConstant.DZO(level 0, pattern DeclConstant.DeclaredConstant 0, id 0) exact DeclConstant.DxO(level 0, pattern DeclConstant.DeclaredConstant xO, id 0) exact DeclConstant.DxI(level 0, pattern DeclConstant.DeclaredConstant xI, id 0) exact DeclConstant.DxH(level 0, pattern DeclConstant.DeclaredConstant 1%positive, id 0) exact DeclConstant.DS(level 0, pattern DeclConstant.DeclaredConstant S, id 0) exact DeclConstant.DO(level 0, pattern DeclConstant.DeclaredConstant 0%nat, id 0) For RewriteRelation -> simple apply @RewriteRelation_instance_2(level 0, pattern RewriteRelation relation_equivalence, id 0) exact RewriteRelation_instance_1(level 0, pattern RewriteRelation iff, id 0) exact RewriteRelation_instance_0(level 0, pattern RewriteRelation Basics.impl, id 0) simple apply @equivalence_rewrite_relation(level 1, pattern RewriteRelation ?META281, id 0) For ZifyClasses.UnOp -> exact ZifyInst.Op_Z_to_pos(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.to_pos, id 0) exact ZifyInst.Op_Z_to_nat(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.to_nat, id 0) exact ZifyInst.Op_Z_quot2(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.quot2, id 0) exact ZifyInst.Op_Z_div2(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.div2, id 0) exact ZifyInst.Op_Z_square(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.square, id 0) exact ZifyInst.Op_Z_succ_double(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.succ_double, id 0) exact ZifyInst.Op_Z_pred_double(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.pred_double, id 0) exact ZifyInst.Op_Z_double(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.double, id 0) exact ZifyInst.Op_Z_sgn(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.sgn, id 0) exact ZifyInst.Op_Z_abs(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.abs, id 0) exact ZifyInst.Op_Z_opp(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.opp, id 0) exact ZifyInst.Op_Z_pred(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.pred, id 0) exact ZifyInst.Op_Z_succ(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.succ, id 0) exact ZifyInst.Op_N_square(level 0, pattern ZifyClasses.UnOp BinNatDef.N.square, id 0) exact ZifyInst.Op_N_div2(level 0, pattern ZifyClasses.UnOp BinNatDef.N.div2, id 0) exact ZifyInst.Op_N_succ_pos(level 0, pattern ZifyClasses.UnOp BinNatDef.N.succ_pos, id 0) exact ZifyInst.Op_N_double(level 0, pattern ZifyClasses.UnOp BinNatDef.N.double, id 0) exact ZifyInst.Op_N_succ_double(level 0, pattern ZifyClasses.UnOp BinNatDef.N.succ_double, id 0) exact ZifyInst.Op_N_succ(level 0, pattern ZifyClasses.UnOp BinNatDef.N.succ, id 0) exact ZifyInst.Op_N_pred(level 0, pattern ZifyClasses.UnOp BinNatDef.N.pred, id 0) exact ZifyInst.Op_N_pos(level 0, pattern ZifyClasses.UnOp N.pos, id 0) exact ZifyInst.Op_Z_abs_N(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.abs_N, id 0) exact ZifyInst.Op_N_of_nat(level 0, pattern ZifyClasses.UnOp BinNatDef.N.of_nat, id 0) exact ZifyInst.Op_N_Npos(level 0, pattern ZifyClasses.UnOp N.pos, id 0) exact ZifyInst.Op_Z_of_nat(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.of_nat, id 0) exact ZifyInst.Op_xI(level 0, pattern ZifyClasses.UnOp xI, id 0) exact ZifyInst.Op_xO(level 0, pattern ZifyClasses.UnOp xO, id 0) exact ZifyInst.Op_Pos_Ndouble(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.Ndouble, id 0) exact ZifyInst.Op_Pos_Nsucc_double(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.Nsucc_double, id 0) exact ZifyInst.Op_pos_square(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.square, id 0) exact ZifyInst.Op_pos_of_nat(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.of_nat, id 0) exact ZifyInst.Op_pos_of_succ_nat(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.of_succ_nat, id 0) exact ZifyInst.Op_pos_predN(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.pred_N, id 0) exact ZifyInst.Op_pos_pred(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.pred, id 0) exact ZifyInst.Op_pos_pred_double(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.pred_double, id 0) exact ZifyInst.Op_pos_succ(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.succ, id 0) exact ZifyInst.Op_Z_pos(level 0, pattern ZifyClasses.UnOp Z.pos, id 0) exact ZifyInst.Op_Z_neg(level 0, pattern ZifyClasses.UnOp (-1), id 0) exact ZifyInst.Op_Z_to_N(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.to_N, id 0) exact ZifyInst.Op_Z_of_N(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.of_N, id 0) exact ZifyInst.Op_N_to_nat(level 0, pattern ZifyClasses.UnOp BinNatDef.N.to_nat, id 0) exact ZifyInst.Op_pos_to_nat(level 0, pattern ZifyClasses.UnOp BinPosDef.Pos.to_nat, id 0) exact ZifyInst.Op_Z_abs_nat(level 0, pattern ZifyClasses.UnOp BinIntDef.Z.abs_nat, id 0) exact ZifyInst.Op_S(level 0, pattern ZifyClasses.UnOp S, id 0) exact ZifyInst.Op_pred(level 0, pattern ZifyClasses.UnOp Init.Nat.pred, id 0) For ZifyClasses.BinOp -> exact ZifyInst.Op_Z_pow_pos(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.pow_pos, id 0) exact ZifyInst.Op_Z_pow(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.pow, id 0) exact ZifyInst.Op_Z_quot(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.quot, id 0) exact ZifyInst.Op_Z_rem(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.rem, id 0) exact ZifyInst.Op_Z_mod(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.modulo, id 0) exact ZifyInst.Op_Z_div(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.div, id 0) exact ZifyInst.Op_Z_sub(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.sub, id 0) exact ZifyInst.Op_Z_mul(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.mul, id 0) exact ZifyInst.Op_Z_max(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.max, id 0) exact ZifyInst.Op_Z_min(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.min, id 0) exact ZifyInst.Op_Z_add(level 0, pattern ZifyClasses.BinOp BinIntDef.Z.add, id 0) exact ZifyInst.Op_N_pow(level 0, pattern ZifyClasses.BinOp BinNatDef.N.pow, id 0) exact ZifyInst.Op_N_mod(level 0, pattern ZifyClasses.BinOp BinNatDef.N.modulo, id 0) exact ZifyInst.Op_N_div(level 0, pattern ZifyClasses.BinOp BinNatDef.N.div, id 0) exact ZifyInst.Op_N_sub(level 0, pattern ZifyClasses.BinOp BinNatDef.N.sub, id 0) exact ZifyInst.Op_N_mul(level 0, pattern ZifyClasses.BinOp BinNatDef.N.mul, id 0) exact ZifyInst.Op_N_max(level 0, pattern ZifyClasses.BinOp BinNatDef.N.max, id 0) exact ZifyInst.Op_N_min(level 0, pattern ZifyClasses.BinOp BinNatDef.N.min, id 0) exact ZifyInst.Op_N_add(level 0, pattern ZifyClasses.BinOp BinNatDef.N.add, id 0) exact ZifyInst.Op_pos_pow(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.pow, id 0) exact ZifyInst.Op_pos_max(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.max, id 0) exact ZifyInst.Op_pos_min(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.min, id 0) exact ZifyInst.Op_pos_mul(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.mul, id 0) exact ZifyInst.Op_pos_sub(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.sub, id 0) exact ZifyInst.Op_pos_add_carry(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.add_carry, id 0) exact ZifyInst.Op_pos_add(level 0, pattern ZifyClasses.BinOp BinPosDef.Pos.add, id 0) exact ZifyInst.Op_max(level 0, pattern ZifyClasses.BinOp Init.Nat.max, id 0) exact ZifyInst.Op_min(level 0, pattern ZifyClasses.BinOp Init.Nat.min, id 0) exact ZifyInst.Op_mul(level 0, pattern ZifyClasses.BinOp Init.Nat.mul, id 0) exact ZifyInst.Op_sub(level 0, pattern ZifyClasses.BinOp Init.Nat.sub, id 0) exact ZifyInst.Op_plus(level 0, pattern ZifyClasses.BinOp Init.Nat.add, id 0) For ZifyClasses.CstOp -> exact ZifyInst.Op_Z_Z0(level 0, pattern ZifyClasses.CstOp 0, id 0) exact ZifyInst.Op_N_N0(level 0, pattern ZifyClasses.CstOp 0%N, id 0) exact ZifyInst.Op_xH(level 0, pattern ZifyClasses.CstOp 1%positive, id 0) exact ZifyInst.Op_O(level 0, pattern ZifyClasses.CstOp 0%nat, id 0) (lift_reflexivity (let env_sym := sigma_get {| Internal.Sym.ar := 0; Internal.Sym.value := b; Internal.Sym.morph := proper_eq b |} (sigma_add 1%positive {| Internal.Sym.ar := 0; Internal.Sym.value := a; Internal.Sym.morph := proper_eq a |} (sigma_empty Internal.Sym.pack)) in let env_bin := sigma_get {| Internal.Bin.value := Z.max; Internal.Bin.compat := Z.max_compat; Internal.Bin.assoc := aac_Zmax_Assoc; Internal.Bin.comm := Some aac_Zmax_Comm; Internal.Bin.idem := Some aac_Zmax_Idem |} (sigma_add 2%positive {| Internal.Bin.value := Z.add; Internal.Bin.compat := reflexive_proper Z.add; Internal.Bin.assoc := aac_Zplus_Assoc; Internal.Bin.comm := Some aac_Zplus_Comm; Internal.Bin.idem := None |} (sigma_empty Internal.Bin.pack)) in let env_units := sigma_get {| Internal.u_value := 0; Internal.u_desc := {| Internal.uf_idx := 2; Internal.uf_desc := aac_zero_Zplus |} :: nil |} (sigma_empty (Internal.unit_pack env_bin)) in let tty := Internal.T env_sym in let rsum := Internal.sum (e_sym:=env_sym) in let rprd := Internal.prd (e_sym:=env_sym) in let rsym := Internal.sym (e_sym:=env_sym) in let vnil := Internal.vnil env_sym in let vcons := Internal.vcons (e_sym:=env_sym) in let eval := Internal.eval (e_sym:=env_sym) env_units in let left := rsum 1%positive (Utils.cons (rsum 2%positive (Utils.cons (rsym 1%positive vnil, 1%positive) (Utils.nil (rsym 2%positive vnil, 1%positive))), 1%positive) (Utils.nil (rsum 2%positive (Utils.cons (rsym 2%positive vnil, 1%positive) (Utils.nil (rsym 1%positive vnil, 1%positive))), 1%positive))) in let right := rsum 2%positive (Utils.cons (rsym 1%positive vnil, 1%positive) (Utils.nil (rsym 2%positive vnil, 1%positive))) in Internal.decide env_units left right (eq_refl : Internal.compare (Internal.norm env_units left) (Internal.norm env_units right) = Eq) <: Z.max (a + b) (b + a) = a + b)) File "./theories/Tutorial.v", line 398, characters 4-37: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (Z.abs a + - Z.abs b + 0)%Z occurrence 1: transitivity through (Z.abs a + - (Z.abs b + 0))%Z occurrence 2: transitivity through (Z.abs a + - Z.abs (b + 0))%Z occurrence 3: transitivity through (- Z.abs b + Z.abs (a + 0))%Z File "./theories/Tutorial.v", line 399, characters 4-40: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing "coqc" -q '-w' '+default' "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" -I src -Q theories AAC_tactics -Q src AAC_tactics theories/Caveats.v All solutions: occurrence 0: transitivity through forall x : Z, (- (x + x) + (b + b + c))%Z 1 possible(s) substitution(s) 0: [x: a; ] occurrence 1: transitivity through forall x : Z, (x + x + (- (a + a) + c))%Z 1 possible(s) substitution(s) 0: [x: b; ] File "./theories/Caveats.v", line 276, characters 4-32: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through dot y 1 occurrence 1: transitivity through dot 1 y File "./theories/Caveats.v", line 277, characters 4-35: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 295, characters 4-18: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 303, characters 4-23: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing File "./theories/Caveats.v", line 327, characters 2-19: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c * b + a + 0)%nat occurrence 1: transitivity through (a + b * (c + 0))%nat occurrence 2: transitivity through (a + c * (b + 0))%nat File "./theories/Caveats.v", line 344, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through (c + b + a + 0)%nat File "./theories/Caveats.v", line 347, characters 2-26: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((c + b + a) * 1)%nat occurrence 1: transitivity through (c + a + b * 1)%nat occurrence 2: transitivity through (a + (c + b) * 1)%nat occurrence 3: transitivity through (b + a + c * 1)%nat occurrence 4: transitivity through (c + (b + a) * 1)%nat occurrence 5: transitivity through (c + b + a * 1)%nat occurrence 6: transitivity through (b + (c + a) * 1)%nat All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] File "./theories/Caveats.v", line 363, characters 2-22: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through forall x y : nat, (x * x + y * x + c)%nat 1 possible(s) substitution(s) 0: [x: a; y: b; ] occurrence 1: transitivity through ((a * b + a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 2: transitivity through (a * b + c + a * a * (1 * 1 + 0 * 1))%nat occurrence 3: transitivity through (c + (a * b + a * a) * (1 * 1 + 0 * 1))%nat occurrence 4: transitivity through (a * a + c + a * b * (1 * 1 + 0 * 1))%nat occurrence 5: transitivity through (a * b + (a * a + c) * (1 * 1 + 0 * 1))%nat occurrence 6: transitivity through (a * b + a * a + c * (1 * 1 + 0 * 1))%nat occurrence 7: transitivity through (a * a + (a * b + c) * (1 * 1 + 0 * 1))%nat File "./theories/Caveats.v", line 366, characters 2-20: Warning: [aac_tactics] This pattern can be instantiated to match units, some solutions can be missing All solutions: occurrence 0: transitivity through ((a * b + a * a + c) * 1)%nat occurrence 1: transitivity through (a * b + c + a * a * 1)%nat occurrence 2: transitivity through (c + (a * b + a * a) * 1)%nat occurrence 3: transitivity through (a * a + c + a * b * 1)%nat occurrence 4: transitivity through (a * b + (a * a + c) * 1)%nat occurrence 5: transitivity through (a * b + a * a + c * 1)%nat occurrence 6: transitivity through (a * a + (a * b + c) * 1)%nat /usr/bin/make --no-print-directory -f "Makefile.coq" post-all make[3]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' mkdir -p html "coqdoc" \ -toc -interpolate -utf8 -html -Q theories AAC_tactics -Q src AAC_tactics -d html theories/Utils.v theories/Constants.v theories/AAC.v theories/Instances.v theories/Tutorial.v theories/Caveats.v make[2]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' make[1]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' dh: command-omitted: The call to "dh_auto_test -a" was omitted due to "DEB_BUILD_OPTIONS=nocheck" create-stamp debian/debhelper-build-stamp dh_prep -a debian/rules override_dh_auto_install make[1]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' /usr/bin/make -f Makefile.coq install install-byte DSTROOT=/build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp make[2]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' code=0; for f in theories/Utils.vo theories/Constants.vo theories/AAC.vo theories/Instances.vo theories/Tutorial.vo theories/Caveats.vo theories/Utils.v theories/Constants.v theories/AAC.v theories/Instances.v theories/Tutorial.v theories/Caveats.v theories/Utils.glob theories/Constants.glob theories/AAC.glob theories/Instances.glob theories/Tutorial.glob theories/Caveats.glob src/aac_plugin.cmi src/aac_plugin.cmxs src/aac_plugin.cmxs src/aac_plugin.cmxa src/aac_plugin.cmx; do\ if ! [ -f "$f" ]; then >&2 echo $f does not exist; code=1; fi \ done; exit $code for f in theories/Utils.vo theories/Constants.vo theories/AAC.vo theories/Instances.vo theories/Tutorial.vo theories/Caveats.vo theories/Utils.v theories/Constants.v theories/AAC.v theories/Instances.v theories/Tutorial.v theories/Caveats.v theories/Utils.glob theories/Constants.glob theories/AAC.glob theories/Instances.glob theories/Tutorial.glob theories/Caveats.glob src/aac_plugin.cmi src/aac_plugin.cmxs src/aac_plugin.cmxs src/aac_plugin.cmxa src/aac_plugin.cmx; do\ df="`"coq_makefile" -destination-of "$f" -I src -Q theories AAC_tactics -Q src AAC_tactics `";\ if [ "$?" != "0" -o -z "$df" ]; then\ echo SKIP "$f" since it has no logical path;\ else\ install -d "/build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df" &&\ install -m 0644 "$f" "/build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df" &&\ echo INSTALL "$f" "/build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df";\ fi;\ done INSTALL theories/Utils.vo /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Constants.vo /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/AAC.vo /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Instances.vo /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Tutorial.vo /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Caveats.vo /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Utils.v /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Constants.v /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/AAC.v /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Instances.v /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Tutorial.v /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Caveats.v /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Utils.glob /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Constants.glob /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/AAC.glob /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Instances.glob /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Tutorial.glob /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL theories/Caveats.glob /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmi /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmxs /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmxs /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmxa /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cmx /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ /usr/bin/make install-extra -f "Makefile.coq" make[3]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' make[3]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' for f in src/aac_plugin.cmo src/aac_plugin.cma; do\ df="`"coq_makefile" -destination-of "$f" -I src -Q theories AAC_tactics -Q src AAC_tactics `";\ if [ "$?" != "0" -o -z "$df" ]; then\ echo SKIP "$f" since it has no logical path;\ else\ install -d "/build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df" &&\ install -m 0644 "$f" "/build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df" &&\ echo INSTALL "$f" "/build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/$df";\ fi;\ done INSTALL src/aac_plugin.cmo /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ INSTALL src/aac_plugin.cma /build/aac-tactics-zBHIhn/aac-tactics-8.15.1/debian/tmp//usr/lib/ocaml/coq//user-contrib/AAC_tactics/ make[2]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' make[1]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' dh_install -a dh_ocamldoc -a Warning: Element Rewrite not found Warning: Element Rewrite not found dh_installdocs -a dh_installchangelogs -a dh_lintian -a dh_perl -a dh_link -a dh_strip_nondeterminism -a dh_compress -a dh_fixperms -a debian/rules override_dh_missing make[1]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' dh_missing --fail-missing make[1]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' dh_strip -a dh_makeshlibs -a dh_shlibdeps -a dh_installdeb -a dh_ocaml -a debian/rules override_dh_gencontrol make[1]: Entering directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' dh_gencontrol -- -VF:CoqABI="8.15.1+4.13.1" dpkg-gencontrol: warning: Depends field of package libaac-tactics-ocaml-dev: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libaac-tactics-ocaml: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package libaac-tactics-ocaml: substitution variable ${shlibs:Depends} used, but is not defined make[1]: Leaving directory '/build/aac-tactics-zBHIhn/aac-tactics-8.15.1' dh_md5sums -a dh_builddeb -a dpkg-deb: building package 'libaac-tactics-ocaml' in '../libaac-tactics-ocaml_8.15.1-2_amd64.deb'. dpkg-deb: building package 'libaac-tactics-ocaml-dbgsym' in '../libaac-tactics-ocaml-dbgsym_8.15.1-2_amd64.deb'. dpkg-deb: building package 'libaac-tactics-ocaml-dev' in '../libaac-tactics-ocaml-dev_8.15.1-2_amd64.deb'. dpkg-genbuildinfo --build=any -O../aac-tactics_8.15.1-2_amd64.buildinfo dpkg-genchanges --build=any -O../aac-tactics_8.15.1-2_amd64.changes dpkg-genchanges: info: binary-only arch-specific upload (source code and arch-indep packages not included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: running special hook: sync-out /build/aac-tactics-zBHIhn /tmp/aac-tactics-8.15.1-2h_x07u3j I: cleaning package lists and apt cache... I: removing tempdir /tmp/mmdebstrap.G3jiAuMRFn... I: success in 550.3501 seconds md5: libaac-tactics-ocaml-dbgsym_8.15.1-2_amd64.deb: OK md5: libaac-tactics-ocaml-dev_8.15.1-2_amd64.deb: OK md5: libaac-tactics-ocaml_8.15.1-2_amd64.deb: OK sha1: libaac-tactics-ocaml-dbgsym_8.15.1-2_amd64.deb: OK sha1: libaac-tactics-ocaml-dev_8.15.1-2_amd64.deb: OK sha1: libaac-tactics-ocaml_8.15.1-2_amd64.deb: OK sha256: libaac-tactics-ocaml-dbgsym_8.15.1-2_amd64.deb: OK sha256: libaac-tactics-ocaml-dev_8.15.1-2_amd64.deb: OK sha256: libaac-tactics-ocaml_8.15.1-2_amd64.deb: OK Checksums: OK