Diff of the two buildlogs: -- --- b1/build.log 2024-11-20 17:25:09.610125021 +0000 +++ b2/build.log 2024-11-20 17:28:08.630007235 +0000 @@ -1,6 +1,7 @@ +W: cgroups are not available on the host, not using them. I: pbuilder: network access will be disabled during build -I: Current time: Wed Nov 20 05:19:57 -12 2024 -I: pbuilder-time-stamp: 1732123197 +I: Current time: Thu Nov 21 07:25:13 +14 2024 +I: pbuilder-time-stamp: 1732123513 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/unstable-reproducible-base.tgz] I: copying local configuration @@ -28,52 +29,83 @@ dpkg-source: info: applying 0001-Increase-timeout-in-test-that-takes-a-bit-longer-on-.patch I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/2340221/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/D01_modify_environment starting +debug: Running on codethink04-arm64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +'/bin/sh' -> '/bin/bash' +lrwxrwxrwx 1 root root 9 Nov 20 17:25 /bin/sh -> /bin/bash +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build/reproducible-path' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='arm64' - DEBIAN_FRONTEND='noninteractive' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:globskipdots:hostcomplete:interactive_comments:patsub_replacement:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_LOADABLES_PATH=/usr/local/lib/bash:/usr/lib/bash:/opt/local/lib/bash:/usr/pkg/lib/bash:/opt/pkg/lib/bash:. + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="2" [2]="32" [3]="1" [4]="release" [5]="aarch64-unknown-linux-gnu") + BASH_VERSION='5.2.32(1)-release' + BUILDDIR=/build/reproducible-path + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=arm64 + DEBIAN_FRONTEND=noninteractive DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=12 ' - DISTRIBUTION='unstable' - HOME='/root' - HOST_ARCH='arm64' + DIRSTACK=() + DISTRIBUTION=unstable + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=aarch64 + HOST_ARCH=arm64 IFS=' ' - INVOCATION_ID='592926c7d6ea4b18b786c70eafd6fdf2' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='2340221' - PS1='# ' - PS2='> ' + LANG=C + LANGUAGE=nl_BE:nl + LC_ALL=C + MACHTYPE=aarch64-unknown-linux-gnu + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnu + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=3930213 PS4='+ ' - PWD='/' - SHELL='/bin/bash' - SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.H2AzX3Al/pbuilderrc_ng4v --distribution unstable --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.H2AzX3Al/b1 --logfile b1/build.log coq-elpi_2.2.3-1.dsc' - SUDO_GID='109' - SUDO_UID='104' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://192.168.101.4:3128' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.H2AzX3Al/pbuilderrc_KuWf --distribution unstable --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/unstable-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.H2AzX3Al/b2 --logfile b2/build.log coq-elpi_2.2.3-1.dsc' + SUDO_GID=109 + SUDO_UID=104 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://192.168.101.4:3128 I: uname -a - Linux codethink02-arm64 6.1.0-27-cloud-arm64 #1 SMP Debian 6.1.115-1 (2024-11-01) aarch64 GNU/Linux + Linux i-capture-the-hostname 6.1.0-27-cloud-arm64 #1 SMP Debian 6.1.115-1 (2024-11-01) aarch64 GNU/Linux I: ls -l /bin lrwxrwxrwx 1 root root 7 Aug 4 21:30 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/2340221/tmp/hooks/D02_print_environment finished +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -220,7 +252,7 @@ Get: 93 http://deb.debian.org/debian unstable/main arm64 libstdio-ocaml-dev arm64 0.17.0-1 [116 kB] Get: 94 http://deb.debian.org/debian unstable/main arm64 libppx-optcomp-ocaml-dev arm64 1:0.17.0-1+b3 [325 kB] Get: 95 http://deb.debian.org/debian unstable/main arm64 ocaml-dune arm64 3.16.0-2+b1 [5534 kB] -Fetched 386 MB in 3s (150 MB/s) +Fetched 386 MB in 1s (276 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.12-minimal:arm64. (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 ... 20084 files and directories currently installed.) @@ -543,8 +575,8 @@ Setting up tzdata (2024b-3) ... Current default time zone: 'Etc/UTC' -Local time is now: Wed Nov 20 17:20:54 UTC 2024. -Universal Time is now: Wed Nov 20 17:20:54 UTC 2024. +Local time is now: Wed Nov 20 17:25:47 UTC 2024. +Universal Time is now: Wed Nov 20 17:25:47 UTC 2024. Run 'dpkg-reconfigure tzdata' if you wish to change it. Setting up autotools-dev (20220109.1) ... @@ -629,7 +661,11 @@ Building tag database... -> Finished parsing the build-deps I: Building the package -I: Running cd /build/reproducible-path/coq-elpi-2.2.3/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../coq-elpi_2.2.3-1_source.changes +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/A99_set_merged_usr starting +Not re-configuring usrmerge for unstable +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/A99_set_merged_usr finished +hostname: Name or service not known +I: Running cd /build/reproducible-path/coq-elpi-2.2.3/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../coq-elpi_2.2.3-1_source.changes dpkg-buildpackage: info: source package coq-elpi dpkg-buildpackage: info: source version 2.2.3-1 dpkg-buildpackage: info: source distribution unstable @@ -699,20 +735,10 @@ Arguments E_AND1 e1 e2 (b1 b2)%bool_scope _ _ Arguments E_OR1 e1 e2 (b1 b2)%bool_scope _ _ Arguments E_EQ1 e1 e2 (n1 n2)%nat_scope _ _ +(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_reduction_surgery.v) +(eq_refl : 2 = (let z := 1 in S z)) (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_generalize.v) 3 + 7 ===> fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))) -(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_record_to_sigma.v) -foo = -{f1 : Type & {f2 : f1 -> Type & forall t : f1, f2 t -> bool}} - : Type -mk_foo = -fun (f1 : Type) (f2 : f1 -> Type) (f3 : forall t : f1, f2 t -> bool) => -existT (fun f4 : Type => {f5 : f4 -> Type & forall t : f4, f5 t -> bool}) f1 - (existT (fun f4 : f1 -> Type => forall t : f1, f4 t -> bool) f2 f3) - : forall (f1 : Type) (f2 : f1 -> Type), - (forall t : f1, f2 t -> bool) -> foo - -Arguments mk_foo f1%type_scope (f2 f3)%function_scope (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_import_projections.v) Notation p2 := (p2 nat 3 x) example_import_projections.p1 nat 3 x : nat @@ -727,17 +753,18 @@ (Build bool false 3 eq_refl eq_refl) = 3 example_import_projections.f1 _ x : bool -(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_reduction_surgery.v) -(eq_refl : 2 = (let z := 1 in S z)) -(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_data_base.v) -The Db contains [phone_prefix USA 1] -Phone prefix for USA is 1 -The Db contains -[phone_prefix USA 1, phone_prefix France 33, phone_prefix Italy 39] -Phone prefix for France is 33 -sweet! -brr -yummy! +(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_record_to_sigma.v) +foo = +{f1 : Type & {f2 : f1 -> Type & forall t : f1, f2 t -> bool}} + : Type +mk_foo = +fun (f1 : Type) (f2 : f1 -> Type) (f3 : forall t : f1, f2 t -> bool) => +existT (fun f4 : Type => {f5 : f4 -> Type & forall t : f4, f5 t -> bool}) f1 + (existT (fun f4 : f1 -> Type => forall t : f1, f4 t -> bool) f2 f3) + : forall (f1 : Type) (f2 : f1 -> Type), + (forall t : f1, f2 t -> bool) -> foo + +Arguments mk_foo f1%type_scope (f2 f3)%function_scope (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_record_expansion.v) f = fun (b : bool) (t : r) => @@ -798,6 +825,15 @@ prod `_` (app [global (const «lt»), c1, c2]) c4 \ app [global (const «lt»), c0, c2] 3 +(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_data_base.v) +The Db contains [phone_prefix USA 1] +Phone prefix for USA is 1 +The Db contains +[phone_prefix USA 1, phone_prefix France 33, phone_prefix Italy 39] +Phone prefix for France is 33 +sweet! +brr +yummy! (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/example_reflexive_tactic.v) normP : forall {T : Type} {e : T} {op : T -> T -> T} {gamma : list T} {t1 t2 : lang}, @@ -1486,7 +1522,7 @@ interp x := some (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]) -The module is «elpi_examples.tutorial_coq_elpi_command.Module28» +The module is «elpi_examples.tutorial_coq_elpi_command.Module17» Box.Box.Box.Box.foo = fun n : nat => n + 2 : nat -> nat @@ -1501,100 +1537,6 @@ File "./examples/tutorial_coq_elpi_command.v", line 643, characters 7-14: Warning: This command does not support this attribute: unknown. [unsupported-attributes,parsing,default] -(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/tutorial_coq_elpi_tactic.v) -Goal: -[decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»))] -|- X0 c0 c1 : -app - [global (indt «eq»), global (indt «nat»), - app - [global (const «Nat.add»), c0, - app [global (indc «S»), global (indc «O»)]], c1] -(I, 0) -conj : forall [A B : Prop], A -> B -> A /\ B - -conj is not universe polymorphic -Arguments conj [A B]%type_scope _ _ -Expands to: Constructor Coq.Init.Logic.conj -(ex_intro (fun t : Prop => True /\ True /\ t) True (conj I (conj I I))) -[int 1, str x, str a b, - trm - (app - [global (indt «eq»), X0, - app [global (indc «S»), global (indc «O»)], global (indc «O»)])] -Using H ?p of type Q -Using H ?p of type Q -Using p of type P -[trm c0, trm c3, trm (app [c2, c3])] -found P -found P /\ P -Goal: [decl c0 `x` (global (indt «nat»))] |- X0 c0 : -app - [global (indt «eq»), global (indt «nat»), - app - [global (const «Nat.add»), c0, - app [global (indc «S»), global (indc «O»)]], global (indc «O»)] -Proof state: - {c0} : decl c0 `x` (global (indt «nat»)) - ?- evar (X1 c0) - (app - [global (indt «eq»), global (indt «nat»), - app - [global (const «Nat.add»), c0, - app [global (indc «S»), global (indc «O»)]], - global (indc «O»)]) (X0 c0) /* suspended on X1, X0 */ -EVARS: - ?X57==[x |- x + 1 = 0] (goal evar) {?Goal} - ?X56==[ |- => fun x : nat => ?Goal] (goal evar) - ?X55==[x |- => nat] (parameter A of eq) - ?X54==[ |- => nat] (type of x) - -SHELF:|| -FUTURE GOALS STACK: - || - -Coq-Elpi mapping: -RAW: -?X57 <-> c0 \ X1 c0 -ELAB: -?X57 <-> X0 - -#goals = 2 -[nabla c0 \ - nabla c1 \ - seal - (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X0 c0 c1) c0 - (X1 c0 c1) []), - nabla c0 \ - nabla c1 \ - seal - (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X2 c0 c1) c1 - (X3 c0 c1) [])] -(fun (P Q : Prop) (p : P) (q : Q) => conj ?Goal (conj ?Goal0 ?Goal1)) -(fun (P Q : Prop) (p : P) (q : Q) => conj ?Goal (conj ?Goal0 ?Goal)) -foo = 46 - : nat -bar = (false :: nil)%list - : list bool -baz = (46%nat :: nil)%list - : list nat -File "./examples/tutorial_coq_elpi_tactic.v", line 631, characters 0-22: -Warning: x is already taken, Elpi will make a name up [lib,elpi,default] -File "./examples/tutorial_coq_elpi_tactic.v", line 741, characters 3-225: -Warning: B is linear: name it _B (discard) or B_ (fresh variable) -[elpi.typecheck,elpi,default] -File "./examples/tutorial_coq_elpi_tactic.v", line 741, characters 3-225: -Warning: A is linear: name it _A (discard) or A_ (fresh variable) -[elpi.typecheck,elpi,default] -File "./examples/tutorial_coq_elpi_tactic.v", line 741, characters 3-225: -Warning: Ctx is linear: name it _Ctx (discard) or Ctx_ (fresh variable) -[elpi.typecheck,elpi,default] -File "./examples/tutorial_coq_elpi_tactic.v", line 842, characters 3-280: -Warning: G2 is linear: name it _G2 (discard) or G2_ (fresh variable) -[elpi.typecheck,elpi,default] -File "./examples/tutorial_coq_elpi_tactic.v", line 842, characters 3-280: -Warning: G1 is linear: name it _G1 (discard) or G1_ (fresh variable) -[elpi.typecheck,elpi,default] (cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/tutorial_coq_elpi_HOAS.v) Query assignments: GRnat = indt «nat» @@ -1949,6 +1891,100 @@ _uvk_21_ = X0 Syntactic constraints: evar (X2) (global (indt «bool»)) X1 /* suspended on X2, X1 */ +(cd _build/default && /usr/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -R examples elpi_examples examples/tutorial_coq_elpi_tactic.v) +Goal: +[decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»))] +|- X0 c0 c1 : +app + [global (indt «eq»), global (indt «nat»), + app + [global (const «Nat.add»), c0, + app [global (indc «S»), global (indc «O»)]], c1] +(I, 0) +conj : forall [A B : Prop], A -> B -> A /\ B + +conj is not universe polymorphic +Arguments conj [A B]%type_scope _ _ +Expands to: Constructor Coq.Init.Logic.conj +(ex_intro (fun t : Prop => True /\ True /\ t) True (conj I (conj I I))) +[int 1, str x, str a b, + trm + (app + [global (indt «eq»), X0, + app [global (indc «S»), global (indc «O»)], global (indc «O»)])] +Using H ?p of type Q +Using H ?p of type Q +Using p of type P +[trm c0, trm c3, trm (app [c2, c3])] +found P +found P /\ P +Goal: [decl c0 `x` (global (indt «nat»))] |- X0 c0 : +app + [global (indt «eq»), global (indt «nat»), + app + [global (const «Nat.add»), c0, + app [global (indc «S»), global (indc «O»)]], global (indc «O»)] +Proof state: + {c0} : decl c0 `x` (global (indt «nat»)) + ?- evar (X1 c0) + (app + [global (indt «eq»), global (indt «nat»), + app + [global (const «Nat.add»), c0, + app [global (indc «S»), global (indc «O»)]], + global (indc «O»)]) (X0 c0) /* suspended on X1, X0 */ +EVARS: + ?X57==[x |- x + 1 = 0] (goal evar) {?Goal} + ?X56==[ |- => fun x : nat => ?Goal] (goal evar) + ?X55==[x |- => nat] (parameter A of eq) + ?X54==[ |- => nat] (type of x) + +SHELF:|| +FUTURE GOALS STACK: + || + +Coq-Elpi mapping: +RAW: +?X57 <-> c0 \ X1 c0 +ELAB: +?X57 <-> X0 + +#goals = 2 +[nabla c0 \ + nabla c1 \ + seal + (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X0 c0 c1) c0 + (X1 c0 c1) []), + nabla c0 \ + nabla c1 \ + seal + (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X2 c0 c1) c1 + (X3 c0 c1) [])] +(fun (P Q : Prop) (p : P) (q : Q) => conj ?Goal (conj ?Goal0 ?Goal1)) +(fun (P Q : Prop) (p : P) (q : Q) => conj ?Goal (conj ?Goal0 ?Goal)) +foo = 46 + : nat +bar = (false :: nil)%list + : list bool +baz = (46%nat :: nil)%list + : list nat +File "./examples/tutorial_coq_elpi_tactic.v", line 631, characters 0-22: +Warning: x is already taken, Elpi will make a name up [lib,elpi,default] +File "./examples/tutorial_coq_elpi_tactic.v", line 741, characters 3-225: +Warning: B is linear: name it _B (discard) or B_ (fresh variable) +[elpi.typecheck,elpi,default] +File "./examples/tutorial_coq_elpi_tactic.v", line 741, characters 3-225: +Warning: A is linear: name it _A (discard) or A_ (fresh variable) +[elpi.typecheck,elpi,default] +File "./examples/tutorial_coq_elpi_tactic.v", line 741, characters 3-225: +Warning: Ctx is linear: name it _Ctx (discard) or Ctx_ (fresh variable) +[elpi.typecheck,elpi,default] +File "./examples/tutorial_coq_elpi_tactic.v", line 842, characters 3-280: +Warning: G2 is linear: name it _G2 (discard) or G2_ (fresh variable) +[elpi.typecheck,elpi,default] +File "./examples/tutorial_coq_elpi_tactic.v", line 842, characters 3-280: +Warning: G1 is linear: name it _G1 (discard) or G1_ (fresh variable) +[elpi.typecheck,elpi,default] (cd _build/default && /usr/bin/coqc -w -all -w -elpi -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ondemand -boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/boot -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/clib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/engine -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/gramlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/interp -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/kernel -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/lib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/library -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/parsing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/perf -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/pretyping -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/printing -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/proofs -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/tactics -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vernac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq-core/vm -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/dynlink -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/lexer_config -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/parser -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/trace/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/elpi/util -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/findlib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/menhirLib -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/ppx_deriving/runtime -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/re/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/seq -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/stdlib-shims -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/str -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/threads -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/unix -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/zarith -I apps/tc/src -I src -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/btauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/cc -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/derive -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/extraction -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/firstorder -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/funind -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ltac2_ltac1 -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/micromega_core -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/nsatz -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/number_string_notation -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ring -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/rtauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssreflect -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/ssrmatching -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/tauto -I /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/../coq-core/plugins/zify -R /usr/lib/aarch64-linux-gnu/ocaml/5.2.0/coq/theories Coq -Q elpi elpi_elpi -Q theories elpi -Q apps/tc/elpi elpi.apps.tc.elpi -R apps/tc/theories elpi.apps.tc apps/tc/theories/tc.v) File "./apps/tc/theories/tc.v", line 205, characters 0-24: Warning: @@ -2323,8 +2359,6 @@ ^^^^^^^^^^^^^^^^^^^^^^^^^ Alert deprecated: Library.indirect_accessor Most commands should not be accessing opaque data. -(eq_refl : 2 = (let z := 1 in S z)) -3 + 7 ===> fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))) foo = {f1 : Type & {f2 : f1 -> Type & forall t : f1, f2 t -> bool}} : Type @@ -2336,6 +2370,7 @@ (forall t : f1, f2 t -> bool) -> foo Arguments mk_foo f1%type_scope (f2 f3)%function_scope +(eq_refl : 2 = (let z := 1 in S z)) Notation p2 := (p2 nat 3 x) example_import_projections.p1 nat 3 x : nat : nat @@ -2382,6 +2417,7 @@ Arguments E_AND1 e1 e2 (b1 b2)%bool_scope _ _ Arguments E_OR1 e1 e2 (b1 b2)%bool_scope _ _ Arguments E_EQ1 e1 e2 (n1 n2)%nat_scope _ _ +3 + 7 ===> fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))) f = fun (b : bool) (t : r) => let q := negb b in @@ -2829,7 +2865,7 @@ rid:1 step:4 gid:20 user:rule:implication = success -}}} -> (0.000s) +}}} -> (0.020s) run 5 {{{ rid:1 step:5 gid:20 user:curgoal = of @@ -3020,7 +3056,7 @@ rid:3 step:5 gid:38 user:rule:backchain = success -}}} -> (0.000s) +}}} -> (0.008s) run 8 {{{ rid:3 step:8 gid:40 user:curgoal = of @@ -3040,7 +3076,7 @@ rid:3 step:8 gid:40 user:rule:backchain = success -}}} -> (0.008s) +}}} -> (0.000s) arr X4 (arr X3 X4) Query assignments: Ty = arr X4 (arr X3 X4) @@ -3076,6 +3112,92 @@ A = X0 B = X0 C = X0 +Hello [str world!] +Hello [int 46] +Hello [str there] +Hello [str my, str friend] +Hello [str this.is.a.qualified.name] +Hello +[trm + (app + [global (indt «eq»), global (indt «nat»), global (indc «O»), + app [global (indc «S»), global (indc «O»)]])] +Hello +[const-decl test + (some + (app + [global (indt «eq»), global (indt «nat»), global (indc «O»), + app [global (indc «S»), global (indc «O»)]])) (arity (sort prop))] +Hello +[indt-decl + (record test (sort (typ «Set»)) Build_test + (field [coercion off, canonical tt] f1 (global (indt «nat»)) c0 \ + field [coercion off, canonical tt] f2 + (app + [global (indt «eq»), global (indt «nat»), c0, + app [global (indc «S»), global (indc «O»)]]) c1 \ end-record))] +The type of +app + [global (indt «eq»), global (indt «nat»), + app [global (indc «S»), global (indc «O»)], global (indc «O»)] is +sort prop +1 = true + : Prop +T= +app + [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], + global (indc «true»)] +T1= +app + [global (indt «eq»), global (indt «nat»), + app [global (indc «S»), global (indc «O»)], + app [global (const «bool2nat»), global (indc «true»)]] +Ty= sort prop +nK_bool = 2 + : nat +nK_False = 0 + : nat +Inductive tree' (A : Set) : Set := + leaf' : tree' A | node' : tree' A -> A -> tree' A -> tree' A. + +Arguments tree' A%type_scope +Arguments leaf' A%type_scope +Arguments node' A%type_scope _ _ _ +bob is 24 years old +alice is 21 years old +bob is 24 years old +alice is 21 years old +[attribute elpi.loc + (leaf-loc + File "./examples/tutorial_coq_elpi_command.v", line 609, column 31, character 17344:), + attribute elpi.phase (leaf-str interp), attribute this (leaf-str ), + attribute more (node [attribute stuff (leaf-str 33)])] +options= +[get-option elpi.loc + File "./examples/tutorial_coq_elpi_command.v", line 642, column 31, character 18180:, + get-option elpi.phase interp, get-option this tt, get-option more.stuff 33] +33 tt +That is all folks! +going from source to target via plane +synterp x := some _ +interp x := +some + (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]) +The module is «elpi_examples.tutorial_coq_elpi_command.Module20» +Box.Box.Box.Box.foo = fun n : nat => n + 2 + : nat -> nat + +Arguments Box.Box.Box.Box.foo n%nat_scope +Module NextModule2 := Struct End +File "./examples/tutorial_coq_elpi_command.v", line 609, characters 2-24: +Warning: This command does not support these attributes: more, this. +[unsupported-attributes,parsing,default] +File "./examples/tutorial_coq_elpi_command.v", line 642, characters 2-24: +Warning: This command does not support these attributes: more, this. +[unsupported-attributes,parsing,default] +File "./examples/tutorial_coq_elpi_command.v", line 643, characters 7-14: +Warning: This command does not support this attribute: unknown. +[unsupported-attributes,parsing,default] Query assignments: GRnat = indt «nat» GRplus = const «Nat.add» @@ -3429,92 +3551,6 @@ _uvk_21_ = X0 Syntactic constraints: evar (X2) (global (indt «bool»)) X1 /* suspended on X2, X1 */ -Hello [str world!] -Hello [int 46] -Hello [str there] -Hello [str my, str friend] -Hello [str this.is.a.qualified.name] -Hello -[trm - (app - [global (indt «eq»), global (indt «nat»), global (indc «O»), - app [global (indc «S»), global (indc «O»)]])] -Hello -[const-decl test - (some - (app - [global (indt «eq»), global (indt «nat»), global (indc «O»), - app [global (indc «S»), global (indc «O»)]])) (arity (sort prop))] -Hello -[indt-decl - (record test (sort (typ «Set»)) Build_test - (field [coercion off, canonical tt] f1 (global (indt «nat»)) c0 \ - field [coercion off, canonical tt] f2 - (app - [global (indt «eq»), global (indt «nat»), c0, - app [global (indc «S»), global (indc «O»)]]) c1 \ end-record))] -The type of -app - [global (indt «eq»), global (indt «nat»), - app [global (indc «S»), global (indc «O»)], global (indc «O»)] is -sort prop -1 = true - : Prop -T= -app - [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], - global (indc «true»)] -T1= -app - [global (indt «eq»), global (indt «nat»), - app [global (indc «S»), global (indc «O»)], - app [global (const «bool2nat»), global (indc «true»)]] -Ty= sort prop -nK_bool = 2 - : nat -nK_False = 0 - : nat -Inductive tree' (A : Set) : Set := - leaf' : tree' A | node' : tree' A -> A -> tree' A -> tree' A. - -Arguments tree' A%type_scope -Arguments leaf' A%type_scope -Arguments node' A%type_scope _ _ _ -bob is 24 years old -alice is 21 years old -bob is 24 years old -alice is 21 years old -[attribute elpi.loc - (leaf-loc - File "./examples/tutorial_coq_elpi_command.v", line 609, column 31, character 17344:), - attribute elpi.phase (leaf-str interp), attribute this (leaf-str ), - attribute more (node [attribute stuff (leaf-str 33)])] -options= -[get-option elpi.loc - File "./examples/tutorial_coq_elpi_command.v", line 642, column 31, character 18180:, - get-option elpi.phase interp, get-option this tt, get-option more.stuff 33] -33 tt -That is all folks! -going from source to target via plane -synterp x := some _ -interp x := -some - (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]) -The module is «elpi_examples.tutorial_coq_elpi_command.Module18» -Box.Box.Box.Box.foo = fun n : nat => n + 2 - : nat -> nat - -Arguments Box.Box.Box.Box.foo n%nat_scope -Module NextModule2 := Struct End -File "./examples/tutorial_coq_elpi_command.v", line 609, characters 2-24: -Warning: This command does not support these attributes: more, this. -[unsupported-attributes,parsing,default] -File "./examples/tutorial_coq_elpi_command.v", line 642, characters 2-24: -Warning: This command does not support these attributes: more, this. -[unsupported-attributes,parsing,default] -File "./examples/tutorial_coq_elpi_command.v", line 643, characters 7-14: -Warning: This command does not support this attribute: unknown. -[unsupported-attributes,parsing,default] Goal: [decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»))] |- X0 c0 c1 : @@ -3931,12 +3967,12 @@ (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] dune build $(find apps -type d -name tests) -d - : nat trying i = i trying elpi_ctx_entry_2_ = elpi_ctx_entry_2_ trying elpi_ctx_entry_1_ = elpi_ctx_entry_1_ /\ p0 = p0 trying elpi_ctx_entry_1_ = elpi_ctx_entry_1_ /\ p0 = p0 +d + : nat Foo.x = 3 : nat Foo.x = 3 @@ -3972,6 +4008,8 @@ : nat A2.B2.f = 2 : nat +Cats.And.Dogs.x = 42 + : nat Inductive listR_inv (A : Type) (PA : A -> Type) (idx0 : list A) : Type := nilR_inv : idx0 = nil -> listR_inv A PA idx0 | consR_inv : forall a : A, @@ -3984,8 +4022,6 @@ Arguments nilR_inv A%type_scope PA%function_scope idx0%list_scope _ Arguments consR_inv A%type_scope PA%function_scope idx0%list_scope a _ xs%list_scope _ _ -Cats.And.Dogs.x = 42 - : nat File "./apps/eltac/tests/test_injection.v", line 15, characters 0-15: Warning: Using Vector.t is known to be technically difficult, see . @@ -4449,6 +4485,13 @@ Solution for C 1 is i1 Goal is E 1 Solution for E 1 is e1 +Now click "Start watching" in the Elpi Trace Browser panel and then execute +the Command/Tactic/Query you want to trace. Also try "F1 Elpi". +(fun H : C Q => + ex_intro (fun T : Type -> Type => forall R : Type -> Type, C R -> C T) Q + (fun (R : Type -> Type) (_ : C R) => let H1 : C Q := H in H1)) +Now click "Start watching" in the Elpi Trace Browser panel and then execute +the Command/Tactic/Query you want to trace. Also try "F1 Elpi". Query assignments: Len = 288 Rules = [tc.instance [] (const «RelationClasses.iff_Symmetric») @@ -4941,13 +4984,6 @@ (indt «RelationClasses.PER»), tc.instance [] (const «ssrsetoid.compat_Reflexive») (const «ssrclasses.Reflexive»)] -Now click "Start watching" in the Elpi Trace Browser panel and then execute -the Command/Tactic/Query you want to trace. Also try "F1 Elpi". -(fun H : C Q => - ex_intro (fun T : Type -> Type => forall R : Type -> Type, C R -> C T) Q - (fun (R : Type -> Type) (_ : C R) => let H1 : C Q := H in H1)) -Now click "Start watching" in the Elpi Trace Browser panel and then execute -the Command/Tactic/Query you want to trace. Also try "F1 Elpi". All the remaining goals are on the shelf. 1 goal @@ -5291,12 +5327,6 @@ (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] (fun x : tele => tele_fmap) -Normalizing app [global (indt «nat2»), global (indc «S»)] -Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] -Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] -Normalizing app [global (indt «nat2»), global (indc «S»)] -Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] -Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] File "./apps/tc/tests/test_tc_declare.v", line 8, characters 2-36: Warning: This command does not fully mirror the watned behavior if the class has methods @@ -5317,6 +5347,12 @@ This command does not fully mirror the watned behavior if the class has methods with implicit arguments (those implicits will be neglected) [[TC] Warning,TC.Declare,elpi,default] +Normalizing app [global (indt «nat2»), global (indc «S»)] +Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] +Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] +Normalizing app [global (indt «nat2»), global (indc «S»)] +Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] +Normalizing app [global (indt «nat2»), global (const «Nat.succ»)] (fun (T : Type) (p : nat -> T -> T -> Prop) (x : T) => partial_app T (p 0) x) eq_refl : @@ -6096,652 +6132,974 @@ There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) rewrite_relation_fun +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (equiv_rewrite_relation R) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (eq_rewrite_relation A) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @PartialOrder_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.flip_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CMorphisms.PartialOrder_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @StrictOrder_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.flip_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CMorphisms.StrictOrder_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.flip_Antisymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.flip_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.complement_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @PartialOrder_inverse) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @StrictOrder_PartialOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @eq_proper_proxy || + class_apply @reflexive_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (not_evar R; class_apply @proper_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) normalizes +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip2) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip1) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (subrelation_tac T U) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply (forall_subrelation B R S); intro) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @subrelation_symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.PartialOrder_inverse) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CMorphisms.StrictOrder_PartialOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip_Transitive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CMorphisms.flip2) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CMorphisms.flip1) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (CMorphisms.subrelation_tac T U) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply (CMorphisms.forall_subrelation B R S); intro) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.subrelation_symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply @CMorphisms.flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CMorphisms.proper_flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.partial_application_tactic +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.proper_subrelation +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.proper_normalization +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.proper_reflexive +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.flip_Transitive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @complement_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip_Asymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply @flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply @complement_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @proper_flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) partial_application_tactic +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) proper_subrelation +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) proper_normalization +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) proper_reflexive +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.flip_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.complement_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.flip_Asymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @irreflexivity) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply flip_Reflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CRelationClasses.irreflexivity) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply CRelationClasses.flip_Reflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) unconvertible +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @CMorphisms.eq_proper_proxy || + class_apply @CMorphisms.reflexive_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (not_evar R; class_apply @CMorphisms.proper_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.normalizes +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip_Antisymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @flip_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (class_apply @complement_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +Warning: +There is an hint extern in the typeclass db: +(*external*) (reflexive_proxy_tac A R) +[elpi.TC.hints,elpi,default] +Received the following event +[str new_instance, str I4, str A, str Export, int -1] +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.rewrite_relation_fun [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (RelationClasses.equiv_rewrite_relation R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.eq_rewrite_relation A) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.eq_proper_proxy || Init.class_apply @Morphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (apply (Morphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (CMorphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (apply (CMorphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (apply @CMorphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.complement_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (apply RelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (apply CRelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) Init.unconvertible [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || Init.class_apply @CMorphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: +File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) rewrite_relation_fun +(*external*) Morphisms.rewrite_relation_fun [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (equiv_rewrite_relation R) +(*external*) (RelationClasses.equiv_rewrite_relation R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (eq_rewrite_relation A) +(*external*) (Morphisms.eq_rewrite_relation A) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip_StrictOrder) +(*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @PartialOrder_StrictOrder) +(*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.flip_StrictOrder) +(*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CMorphisms.PartialOrder_StrictOrder) +(*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip_PreOrder) +(*external*) (Init.class_apply @RelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @StrictOrder_PreOrder) +(*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.flip_PreOrder) +(*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CMorphisms.StrictOrder_PreOrder) +(*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.flip_Antisymmetric) +(*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.flip_Symmetric) +(*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.complement_Symmetric) +(*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @PartialOrder_inverse) +(*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @StrictOrder_PartialOrder) +(*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @eq_proper_proxy || - class_apply @reflexive_proper_proxy) +(*external*) (Init.class_apply @Morphisms.eq_proper_proxy || + Init.class_apply @Morphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (not_evar R; class_apply @proper_proper_proxy) +(*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) normalizes +(*external*) Morphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip2) +(*external*) (Init.class_apply @Morphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip1) +(*external*) (Init.class_apply @Morphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (subrelation_tac T U) +(*external*) (Morphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (apply (forall_subrelation B R S); intro) +(*external*) (apply (Morphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @subrelation_symmetric) +(*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.PartialOrder_inverse) +(*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CMorphisms.StrictOrder_PartialOrder) +(*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip_Transitive) +(*external*) (Init.class_apply @RelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CMorphisms.flip2) +(*external*) (Init.class_apply @CMorphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CMorphisms.flip1) +(*external*) (Init.class_apply @CMorphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (CMorphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply (CMorphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.subrelation_symmetric) +(*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @CMorphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CMorphisms.proper_flip_proper) +(*external*) (Init.class_apply @CMorphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.flip_Transitive) +(*external*) (Init.class_apply @CRelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip_Irreflexive) +(*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @complement_Irreflexive) +(*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip_Asymmetric) +(*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (apply @flip_proper) +(*external*) (apply @Morphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (apply @complement_proper) +(*external*) (apply @Morphisms.complement_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @proper_flip_proper) +(*external*) (Init.class_apply @Morphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) partial_application_tactic +(*external*) Morphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) proper_subrelation +(*external*) Morphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) proper_normalization +(*external*) Morphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) proper_reflexive +(*external*) Morphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.flip_Irreflexive) +(*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.complement_Irreflexive) +(*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.flip_Asymmetric) +(*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @irreflexivity) +(*external*) (Init.class_apply @RelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (apply flip_Reflexive) +(*external*) (apply RelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CRelationClasses.irreflexivity) +(*external*) (Init.class_apply @CRelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply CRelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) unconvertible +(*external*) Init.unconvertible [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @CMorphisms.eq_proper_proxy || - class_apply @CMorphisms.reflexive_proper_proxy) +(*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || + Init.class_apply @CMorphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (not_evar R; class_apply @CMorphisms.proper_proper_proxy) +(*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip_Antisymmetric) +(*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @flip_Symmetric) +(*external*) (Init.class_apply @RelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (class_apply @complement_Symmetric) +(*external*) (Init.class_apply @RelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/stdppInj.v", line 11, characters 0-24: +File "./apps/tc/tests/importOrder/f2a.v", line 10, characters 0-21: Warning: There is an hint extern in the typeclass db: -(*external*) (reflexive_proxy_tac A R) +(*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -Received the following event -[str new_instance, str I4, str A, str Export, int -1] File "./apps/tc/tests/importOrder/f3f.v", line 7, characters 2-23: Warning: There is an hint extern in the typeclass db: @@ -7708,6 +8066,336 @@ There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] +Debug: [elpitime] Elpi: get_and_compile 0.0000 +Debug: [TC] - Time of instance search is 0.000075 +Debug: [TC] - Time of refine.typecheck is 0.000221 +Debug: +[elpitime] + Elpi: query-compilation:0.0002 static-check:0.0000 optimization:0.0117 runtime:0.0019 (with success) + +Finished transaction in 0.014 secs (0.01u,0.s) (successful) +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) Morphisms.rewrite_relation_fun +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (RelationClasses.equiv_rewrite_relation R) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Morphisms.eq_rewrite_relation A) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.flip_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @Morphisms.eq_proper_proxy || + Init.class_apply @Morphisms.reflexive_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) Morphisms.normalizes +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @Morphisms.flip2) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @Morphisms.flip1) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Morphisms.subrelation_tac T U) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply (Morphisms.forall_subrelation B R S); intro) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.flip_Transitive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CMorphisms.flip2) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CMorphisms.flip1) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (CMorphisms.subrelation_tac T U) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply (CMorphisms.forall_subrelation B R S); intro) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply @CMorphisms.flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CMorphisms.proper_flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.partial_application_tactic +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.proper_subrelation +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.proper_normalization +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.proper_reflexive +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.flip_Transitive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply @Morphisms.flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply @Morphisms.complement_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @Morphisms.proper_flip_proper) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) Morphisms.partial_application_tactic +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) Morphisms.proper_subrelation +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) Morphisms.proper_normalization +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) Morphisms.proper_reflexive +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.irreflexivity) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply RelationClasses.flip_Reflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CRelationClasses.irreflexivity) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (apply CRelationClasses.flip_Reflexive) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) Init.unconvertible +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || + Init.class_apply @CMorphisms.reflexive_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) CMorphisms.normalizes +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.flip_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Init.class_apply @RelationClasses.complement_Symmetric) +[elpi.TC.hints,elpi,default] +File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +Warning: +There is an hint extern in the typeclass db: +(*external*) (Morphisms.reflexive_proxy_tac A R) +[elpi.TC.hints,elpi,default] File "./apps/tc/tests/importOrder/f3c.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: @@ -9962,968 +10650,968 @@ There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.rewrite_relation_fun [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (RelationClasses.equiv_rewrite_relation R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.eq_rewrite_relation A) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.eq_proper_proxy || Init.class_apply @Morphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply (Morphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (CMorphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply (CMorphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @CMorphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.complement_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply RelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply CRelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Init.unconvertible [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || Init.class_apply @CMorphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3g.v", line 8, characters 2-23: +File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.rewrite_relation_fun [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (RelationClasses.equiv_rewrite_relation R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.eq_rewrite_relation A) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.eq_proper_proxy || Init.class_apply @Morphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply (Morphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (CMorphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply (CMorphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @CMorphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.complement_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply RelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply CRelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Init.unconvertible [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || Init.class_apply @CMorphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.rewrite_relation_fun [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (RelationClasses.equiv_rewrite_relation R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.eq_rewrite_relation A) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.eq_proper_proxy || Init.class_apply @Morphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply (Morphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip2) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.flip1) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (CMorphisms.subrelation_tac T U) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply (CMorphisms.forall_subrelation B R S); intro) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @CMorphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Transitive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply @Morphisms.complement_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @Morphisms.proper_flip_proper) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.partial_application_tactic [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_subrelation [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_normalization [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Morphisms.proper_reflexive [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply RelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CRelationClasses.irreflexivity) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (apply CRelationClasses.flip_Reflexive) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) Init.unconvertible [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || Init.class_apply @CMorphisms.reflexive_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) CMorphisms.normalizes [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.flip_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Init.class_apply @RelationClasses.complement_Symmetric) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3a.v", line 4, characters 0-21: +File "./apps/tc/tests/importOrder/f3b.v", line 4, characters 0-21: Warning: There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) @@ -12538,658 +13226,6 @@ There is an hint extern in the typeclass db: (*external*) (Morphisms.reflexive_proxy_tac A R) [elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.rewrite_relation_fun -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (RelationClasses.equiv_rewrite_relation R) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Morphisms.eq_rewrite_relation A) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.eq_proper_proxy || - Init.class_apply @Morphisms.reflexive_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.normalizes -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.flip2) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.flip1) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Morphisms.subrelation_tac T U) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply (Morphisms.forall_subrelation B R S); intro) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Transitive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.flip2) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.flip1) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (CMorphisms.subrelation_tac T U) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply (CMorphisms.forall_subrelation B R S); intro) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply @CMorphisms.flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.proper_flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.partial_application_tactic -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.proper_subrelation -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.proper_normalization -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.proper_reflexive -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Transitive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply @Morphisms.flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply @Morphisms.complement_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.proper_flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.partial_application_tactic -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.proper_subrelation -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.proper_normalization -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.proper_reflexive -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.irreflexivity) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply RelationClasses.flip_Reflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.irreflexivity) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply CRelationClasses.flip_Reflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Init.unconvertible -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || - Init.class_apply @CMorphisms.reflexive_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.normalizes -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.complement_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 7, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Morphisms.reflexive_proxy_tac A R) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.rewrite_relation_fun -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (RelationClasses.equiv_rewrite_relation R) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Morphisms.eq_rewrite_relation A) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.PartialOrder_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.PartialOrder_StrictOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.StrictOrder_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.StrictOrder_PreOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Antisymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.complement_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.PartialOrder_inverse) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.StrictOrder_PartialOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.eq_proper_proxy || - Init.class_apply @Morphisms.reflexive_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (not_evar R; Init.class_apply @Morphisms.proper_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.normalizes -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.flip2) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.flip1) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Morphisms.subrelation_tac T U) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply (Morphisms.forall_subrelation B R S); intro) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.subrelation_symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.PartialOrder_inverse) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.StrictOrder_PartialOrder) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Transitive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.flip2) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.flip1) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (CMorphisms.subrelation_tac T U) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply (CMorphisms.forall_subrelation B R S); intro) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.subrelation_symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply @CMorphisms.flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.proper_flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.partial_application_tactic -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.proper_subrelation -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.proper_normalization -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.proper_reflexive -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Transitive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.complement_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Asymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply @Morphisms.flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply @Morphisms.complement_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @Morphisms.proper_flip_proper) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.partial_application_tactic -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.proper_subrelation -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.proper_normalization -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Morphisms.proper_reflexive -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.complement_Irreflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.flip_Asymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.irreflexivity) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply RelationClasses.flip_Reflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CRelationClasses.irreflexivity) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (apply CRelationClasses.flip_Reflexive) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) Init.unconvertible -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @CMorphisms.eq_proper_proxy || - Init.class_apply @CMorphisms.reflexive_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (not_evar R; Init.class_apply @CMorphisms.proper_proper_proxy) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) CMorphisms.normalizes -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Antisymmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.flip_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Init.class_apply @RelationClasses.complement_Symmetric) -[elpi.TC.hints,elpi,default] -File "./apps/tc/tests/importOrder/f3e.v", line 24, characters 0-21: -Warning: -There is an hint extern in the typeclass db: -(*external*) (Morphisms.reflexive_proxy_tac A R) -[elpi.TC.hints,elpi,default] -Debug: [elpitime] Elpi: get_and_compile 0.0000 -Debug: [TC] - Time of instance search is 0.000076 -Debug: [TC] - Time of refine.typecheck is 0.000239 -Debug: -[elpitime] - Elpi: query-compilation:0.0002 static-check:0.0000 optimization:0.0318 runtime:0.0142 (with success) - -Finished transaction in 0.046 secs (0.01u,0.s) (successful) File "./apps/tc/tests/importOrder/f4.v", line 8, characters 0-21: Warning: There is an hint extern in the typeclass db: @@ -13528,13 +13564,13 @@ Skipping derivation tag on indt «nat» since it has been already run Skipping derivation eqType_ast on indt «nat» since it has been already run Derivation projK on indt «nat» -Derivation projK on indt «nat» took 0.013178 +Derivation projK on indt «nat» took 0.001116 Derivation isK on indt «nat» -Derivation isK on indt «nat» took 0.001807 +Derivation isK on indt «nat» took 0.001835 Derivation eq on indt «nat» -Derivation eq on indt «nat» took 0.013500 +Derivation eq on indt «nat» took 0.005759 Derivation invert on indt «nat» -Derivation invert on indt «nat» took 0.001309 +Derivation invert on indt «nat» took 0.001393 Skipping derivation lens_laws on indt «nat» since it has been already run Skipping derivation param1_congr on indt «nat» since it has been already run @@ -13544,7 +13580,7 @@ since it has been already run Skipping derivation fields on indt «nat» since it has been already run Derivation bcongr on indt «nat» -Derivation bcongr on indt «nat» took 0.014621 +Derivation bcongr on indt «nat» took 0.014796 Derivation idx2inv on indt «nat» Derivation idx2inv on indt «nat» failed, continuing Skipping derivation param1_trivial on indt «nat» @@ -13552,13 +13588,13 @@ Skipping derivation induction on indt «nat» since it has been already run Skipping derivation eqb on indt «nat» since it has been already run Derivation eqK on indt «nat» -Derivation eqK on indt «nat» took 0.015093 +Derivation eqK on indt «nat» took 0.003254 Skipping derivation eqbcorrect on indt «nat» since it has been already run Derivation eqcorrect on indt «nat» Derivation eqcorrect on indt «nat» took 0.000910 Skipping derivation eqbOK on indt «nat» since it has been already run Derivation eqOK on indt «nat» -Derivation eqOK on indt «nat» took 0.000568 +Derivation eqOK on indt «nat» took 0.008617 Skipping derivation map on indt «nat» since the user did not select it Skipping derivation lens on indt «nat» since the user did not select it Skipping derivation param1 on indt «nat» since it has been already run @@ -14037,7 +14073,7 @@ _uvk_3_ = X2 _uvk_4_ = X3 _uvk_5_ = X4 -Finished transaction in 0.457 secs (0.077u,0.007s) (successful) +Finished transaction in 0.172 secs (0.084u,0.s) (successful) Query assignments: A = c0 \ c0 @@ -14326,12 +14362,14 @@ dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: including full source code in upload I: copying local configuration +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/3930213/tmp/hooks/B01_cleanup finished I: unmounting dev/ptmx filesystem I: unmounting dev/pts filesystem I: unmounting dev/shm filesystem I: unmounting proc filesystem I: unmounting sys filesystem I: cleaning the build env -I: removing directory /srv/workspace/pbuilder/2340221 and its subdirectories -I: Current time: Wed Nov 20 05:25:08 -12 2024 -I: pbuilder-time-stamp: 1732123508 +I: removing directory /srv/workspace/pbuilder/3930213 and its subdirectories +I: Current time: Thu Nov 21 07:28:07 +14 2024 +I: pbuilder-time-stamp: 1732123687