Mock Version: 3.5
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs  --target s390x --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/fedora-rawhide-s390x-1672233395.877691/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x3ff9af00410>timeout=0uid=1001gid=135user='mockbuild'nspawn_args=['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.mrydv1k0:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']unshare_net=TrueprintOutput=True)
Using nspawn with args ['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.mrydv1k0:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']
Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', 'fed1fca0b6734ff6954f241a01f2c548', '-D', '/var/lib/mock/fedora-rawhide-s390x-1672233395.877691/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.mrydv1k0:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;<mock-chroot>\\007"', '--setenv=PS1=<mock-chroot> \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bs  --target s390x --nodeps /builddir/build/SPECS/flocq.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False
Building target platforms: s390x
Building for target s390x
setting SOURCE_DATE_EPOCH=1669420800
Wrote: /builddir/build/SRPMS/flocq-4.1.0-2.fc38.src.rpm
Child return code was: 0
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb  --target s390x --nodeps /builddir/build/SPECS/flocq.spec'], chrootPath='/var/lib/mock/fedora-rawhide-s390x-1672233395.877691/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x3ff9af00410>timeout=0uid=1001gid=135user='mockbuild'nspawn_args=['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.mrydv1k0:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']unshare_net=TrueprintOutput=True)
Using nspawn with args ['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.mrydv1k0:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']
Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', 'd40c2ff47b8a4ccfa2bdae88f58a37a8', '-D', '/var/lib/mock/fedora-rawhide-s390x-1672233395.877691/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.mrydv1k0:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/mapper/control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;<mock-chroot>\\007"', '--setenv=PS1=<mock-chroot> \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bb  --target s390x --nodeps /builddir/build/SPECS/flocq.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False
Building target platforms: s390x
Building for target s390x
setting SOURCE_DATE_EPOCH=1669420800
Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.16yGFP
+ umask 022
+ cd /builddir/build/BUILD
+ cd /builddir/build/BUILD
+ rm -rf flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5
+ /usr/lib/rpm/rpmuncompress -x /builddir/build/SOURCES/flocq-4.1.0.tar.gz
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ sed -i 's,\(--coqlib \)[^[:blank:]]*,\1/usr/lib64/ocaml/coq,' Remakefile.in
+ sed -i 's/@COQC@.* -R src Flocq/& -native-compiler yes/' Remakefile.in
+ autoconf -f
configure.in:5: warning: prefer named diversions
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.sdQxBn
+ umask 022
+ cd /builddir/build/BUILD
+ CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection'
+ export CFLAGS
+ CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection'
+ export CXXFLAGS
+ FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules'
+ export FFLAGS
+ FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules'
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed  -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 '
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5
+ ./configure
checking for coqc... /usr/bin/coqc
checking Coq version... 8.16.1
checking for coqdep... /usr/bin/coqdep
checking for coqdoc... /usr/bin/coqdoc
checking whether the C++ compiler works... yes
checking for C++ compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C++... yes
checking whether g++ accepts -g... yes
checking for g++ option to enable C++11 features... none needed
configure: building remake...
/usr/bin/ld: /tmp/ccz93Nkc.o: in function `main':
remake.cpp:(.text.startup+0xb1c): warning: the use of `tempnam' is dangerous, better use `mkstemp'
configure: creating ./config.status
config.status: creating Remakefile
config.status: creating src/Version.v
config.status: creating src/IEEE754/Int63Compat.v
+ rm -f remake
+ ln -s /usr/bin/remake remake
+ remake -d -j2 all doc
Building src/Version.vo
Building src/Core/Raux.vo
/usr/bin/coqdep -R src Flocq src/Version.v | ./remake -r src/Version.vo
/usr/bin/coqdep -R src Flocq src/Core/Raux.v | ./remake -r src/Core/Raux.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Version.v
Building src/Core/Zaux.vo
/usr/bin/coqdep -R src Flocq src/Core/Zaux.v | ./remake -r src/Core/Zaux.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Zaux.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Version.vo
Building src/Core/Defs.vo
/usr/bin/coqdep -R src Flocq src/Core/Defs.v | ./remake -r src/Core/Defs.vo
Building src/Core/Digits.vo
/usr/bin/coqdep -R src Flocq src/Core/Digits.v | ./remake -r src/Core/Digits.vo
Building src/Core/Float_prop.vo
/usr/bin/coqdep -R src Flocq src/Core/Float_prop.v | ./remake -r src/Core/Float_prop.vo
Building src/Core/FIX.vo
/usr/bin/coqdep -R src Flocq src/Core/FIX.v | ./remake -r src/Core/FIX.vo
Building src/Core/Generic_fmt.vo
/usr/bin/coqdep -R src Flocq src/Core/Generic_fmt.v | ./remake -r src/Core/Generic_fmt.vo
Building src/Core/Round_pred.vo
/usr/bin/coqdep -R src Flocq src/Core/Round_pred.v | ./remake -r src/Core/Round_pred.vo
Building src/Core/Round_NE.vo
/usr/bin/coqdep -R src Flocq src/Core/Round_NE.v | ./remake -r src/Core/Round_NE.vo
Building src/Core/Ulp.vo
/usr/bin/coqdep -R src Flocq src/Core/Ulp.v | ./remake -r src/Core/Ulp.vo
Building src/Core/FLT.vo
/usr/bin/coqdep -R src Flocq src/Core/FLT.v | ./remake -r src/Core/FLT.vo
Building src/Core/FLX.vo
/usr/bin/coqdep -R src Flocq src/Core/FLX.v | ./remake -r src/Core/FLX.vo
Building src/Core/FTZ.vo
/usr/bin/coqdep -R src Flocq src/Core/FTZ.v | ./remake -r src/Core/FTZ.vo
Building src/Core/Core.vo
/usr/bin/coqdep -R src Flocq src/Core/Core.v | ./remake -r src/Core/Core.vo
Building src/Calc/Bracket.vo
/usr/bin/coqdep -R src Flocq src/Calc/Bracket.v | ./remake -r src/Calc/Bracket.vo
Building src/Calc/Div.vo
/usr/bin/coqdep -R src Flocq src/Calc/Div.v | ./remake -r src/Calc/Div.vo
Building src/Calc/Operations.vo
/usr/bin/coqdep -R src Flocq src/Calc/Operations.v | ./remake -r src/Calc/Operations.vo
File "./src/Core/Zaux.v", line 991, characters 12-20:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 991, characters 12-20:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 991, characters 12-20:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
Building src/Calc/Plus.vo
/usr/bin/coqdep -R src Flocq src/Calc/Plus.v | ./remake -r src/Calc/Plus.vo
File "./src/Core/Zaux.v", line 1015, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1015, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1015, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1021, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1021, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Zaux.v", line 1021, characters 8-16:
Warning: Notation plus_0_r is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_0_r instead.
[deprecated-syntactic-definition,deprecated]
Building src/Calc/Round.vo
/usr/bin/coqdep -R src Flocq src/Calc/Round.v | ./remake -r src/Calc/Round.vo
Building src/Calc/Sqrt.vo
/usr/bin/coqdep -R src Flocq src/Calc/Sqrt.v | ./remake -r src/Calc/Sqrt.vo
Building src/Prop/Div_sqrt_error.vo
/usr/bin/coqdep -R src Flocq src/Prop/Div_sqrt_error.v | ./remake -r src/Prop/Div_sqrt_error.vo
Building src/Prop/Mult_error.vo
/usr/bin/coqdep -R src Flocq src/Prop/Mult_error.v | ./remake -r src/Prop/Mult_error.vo
Finished src/Core/Zaux.vo
Building src/Prop/Relative.vo
/usr/bin/coqdep -R src Flocq src/Prop/Relative.v | ./remake -r src/Prop/Relative.vo
Building src/Prop/Plus_error.vo
/usr/bin/coqdep -R src Flocq src/Prop/Plus_error.v | ./remake -r src/Prop/Plus_error.vo
Building src/Prop/Sterbenz.vo
/usr/bin/coqdep -R src Flocq src/Prop/Sterbenz.v | ./remake -r src/Prop/Sterbenz.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Digits.v
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Raux.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Core/Raux.v", line 1284, characters 8-24:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1284, characters 8-24:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1284, characters 8-24:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1319, characters 35-47:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1325, characters 54-66:
Warning: Notation Ropp_div_den is deprecated since 8.16. Use Rdiv_opp_r.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 1429, characters 15-30:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2078, characters 10-19:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2279, characters 8-15:
Warning: Notation lt_0_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2279, characters 8-15:
Warning: Notation lt_0_Sn is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_0_succ instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2293, characters 28-34:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2293, characters 28-34:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2343, characters 14-29:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2348, characters 8-14:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2348, characters 8-14:
Warning: Notation le_0_n is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_0_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Core/Raux.v", line 2375, characters 12-27:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/Raux.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Defs.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
/usr/bin/coqdep -R src Flocq src/Prop/Round_odd.v | ./remake -r src/Prop/Round_odd.vo
Finished src/Core/Digits.vo
Building src/Prop/Round_odd.vo
Building src/Prop/Double_rounding.vo
/usr/bin/coqdep -R src Flocq src/Prop/Double_rounding.v | ./remake -r src/Prop/Double_rounding.vo
Finished src/Core/Defs.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Round_pred.v
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Float_prop.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Float_prop.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Calc/Operations.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Round_pred.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Calc/Bracket.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Calc/Operations.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Generic_fmt.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
File "./src/Calc/Bracket.v", line 654, characters 15-27:
Warning: Notation Z_div_mod_eq is deprecated since 8.14.
Use Z_div_mod_eq_full instead [deprecated-syntactic-definition,deprecated]
Finished src/Calc/Bracket.vo
Building src/IEEE754/BinarySingleNaN.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/BinarySingleNaN.v | ./remake -r src/IEEE754/BinarySingleNaN.vo
Building src/IEEE754/Binary.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Binary.v | ./remake -r src/IEEE754/Binary.vo
Building src/IEEE754/Bits.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Bits.v | ./remake -r src/IEEE754/Bits.vo
Building src/IEEE754/Int63Compat.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Int63Compat.v | ./remake -r src/IEEE754/Int63Compat.vo
Building src/IEEE754/Int63Copy.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/Int63Copy.v | ./remake -r src/IEEE754/Int63Copy.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/IEEE754/Int63Copy.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/IEEE754/Int63Copy.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/IEEE754/Int63Compat.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Generic_fmt.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Prop/Sterbenz.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/IEEE754/Int63Compat.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Calc/Sqrt.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Prop/Sterbenz.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Calc/Div.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Calc/Sqrt.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Ulp.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Calc/Div.vo
Building src/IEEE754/PrimFloat.vo
/usr/bin/coqdep -R src Flocq src/IEEE754/PrimFloat.v | ./remake -r src/IEEE754/PrimFloat.vo
Building src/Pff/Pff.vo
/usr/bin/coqdep -R src Flocq src/Pff/Pff.v | ./remake -r src/Pff/Pff.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Pff/Pff.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff.v", line 107, characters 6-14:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 107, characters 6-14:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 241, characters 21-29:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 241, characters 21-29:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 243, characters 6-17:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 243, characters 6-17:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 456, characters 6-14:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 456, characters 6-14:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 464, characters 21-32:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 464, characters 21-32:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 632, characters 25-33:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 632, characters 25-33:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 633, characters 18-29:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 633, characters 18-29:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 655, characters 20-28:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 655, characters 20-28:
Warning: Notation le_or_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_gt_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 673, characters 6-17:
Warning: Notation lt_le_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 673, characters 6-17:
Warning: Notation lt_le_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 714, characters 6-15:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 714, characters 6-15:
Warning: Notation le_not_lt is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.le_ngt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 790, characters 6-19:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 790, characters 6-19:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 791, characters 8-23:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 792, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 810, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 811, characters 11-19:
Warning: Notation Rinv_pow is deprecated since 8.16. Use pow_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 815, characters 8-17:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 879, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 880, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 881, characters 8-23:
Warning: Notation Rinv_involutive is deprecated since 8.16. Use Rinv_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 882, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 882, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 888, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 889, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 889, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 898, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 899, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 900, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 900, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 906, characters 27-42:
Warning: Notation le_plus_minus_r is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 907, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 907, characters 6-16:
Warning: Notation lt_le_weak is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_le_incl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 912, characters 6-21:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 912, characters 6-21:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 922, characters 8-19:
Warning: Notation powerRZ_neg is deprecated since 8.16.
Use powerRZ_neg' and powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 922, characters 8-19:
Warning: Notation powerRZ_neg is deprecated since 8.16.
Use powerRZ_neg' and powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 922, characters 8-19:
Warning: Notation powerRZ_neg is deprecated since 8.16.
Use powerRZ_neg' and powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 923, characters 10-21:
Warning: Notation powerRZ_inv is deprecated since 8.16. Use powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 923, characters 10-21:
Warning: Notation powerRZ_inv is deprecated since 8.16. Use powerRZ_inv'.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 996, characters 22-37:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/Ulp.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Round_NE.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Round_NE.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/FIX.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/FIX.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/FLX.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff.v", line 2323, characters 18-28:
Warning: Notation le_antisym is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_antisymm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2323, characters 18-28:
Warning: Notation le_antisym is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_antisymm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2337, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2337, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2337, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2490, characters 6-12:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2490, characters 20-30:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2490, characters 6-12:
Warning: Notation lt_S_n is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.succ_lt_mono instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2490, characters 20-30:
Warning: Notation le_lt_n_Sm is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_r instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2498, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2498, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2498, characters 8-17:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2591, characters 6-14:
Warning: Notation le_trans is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2591, characters 6-14:
Warning: Notation le_trans is deprecated since 8.16.
The Arith.Le file is obsolete. Use Nat.le_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2593, characters 11-24:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2593, characters 11-24:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2593, characters 11-24:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2593, characters 11-24:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2637, characters 6-19:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 2637, characters 6-19:
Warning: Notation le_plus_minus is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_add (together with Nat.add_comm) instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/FLX.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/FTZ.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/FTZ.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/FLT.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff.v", line 3809, characters 52-59:
Warning: Notation lt_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_lt_pred instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 3809, characters 52-59:
Warning: Notation lt_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_succ_lt_pred instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Core/FLT.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Core/Core.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Core/Core.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Prop/Double_rounding.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5348, characters 56-65:
Warning: Notation mult_comm is deprecated since 8.16.
The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5353, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5372, characters 28-37:
Warning: Notation plus_comm is deprecated since 8.16.
The Arith.Plus file is obsolete. Use Nat.add_comm instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5413, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5417, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5413, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5417, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5429, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5433, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5429, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5433, characters 7-18:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5489, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5494, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5489, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5494, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5504, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5508, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5504, characters 7-20:
Warning: Notation plus_lt_reg_l is deprecated since 8.16.
The Arith.Plus file is obsolete. Use the bidirectional version Nat.add_lt_mono_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 5508, characters 7-15:
Warning: Notation lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 6081, characters 24-32:
Warning: Notation lt_O_neq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 6081, characters 24-32:
Warning: Notation lt_O_neq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.neq_0_lt_0 (together with Nat.neq_sym) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 3492, characters 10-25:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4323, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Double_rounding.v", line 4352, characters 28-44:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Double_rounding.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Prop/Round_odd.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Prop/Round_odd.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Prop/Relative.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Prop/Relative.v", line 568, characters 17-26:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 568, characters 17-26:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 568, characters 17-26:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 572, characters 43-52:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 572, characters 43-52:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Relative.v", line 572, characters 43-52:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Relative.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Prop/Plus_error.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Prop/Plus_error.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Prop/Mult_error.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Prop/Mult_error.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Prop/Div_sqrt_error.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 182, characters 11-19:
Warning: Notation Rsqr_div is deprecated since 8.16. Use Rsqr_div'.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 522, characters 42-51:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Prop/Div_sqrt_error.v", line 691, characters 11-20:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
Finished src/Prop/Div_sqrt_error.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Calc/Round.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11655, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11699, characters 2-17:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
Finished src/Calc/Round.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/IEEE754/BinarySingleNaN.v
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11809, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11905, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 11937, characters 36-51:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12025, characters 8-23:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12038, characters 15-30:
Warning: Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2207, characters 11-27:
Warning: Notation Ropp_inv_permute is deprecated since 8.16. Use Rinv_opp.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2249, characters 21-30:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2258, characters 34-43:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/BinarySingleNaN.v", line 2259, characters 47-56:
Warning: Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12940, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12940, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12940, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 12940, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
Finished src/IEEE754/BinarySingleNaN.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/IEEE754/PrimFloat.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/IEEE754/PrimFloat.v", line 271, characters 10-15:
Warning: Notation ldexp is deprecated since 8.15.0. Use Z.ldexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 278, characters 8-18:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 305, characters 16-21:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 309, characters 12-22:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 309, characters 12-22:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 310, characters 9-14:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 332, characters 0-13:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 332, characters 0-13:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 364, characters 5-10:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 364, characters 5-10:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 381, characters 14-24:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 381, characters 14-24:
Warning: Notation frexp_spec is deprecated since 8.15.0.
Use Z_frexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 383, characters 7-12:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 383, characters 7-12:
Warning: Notation frexp is deprecated since 8.15.0. Use Z.frexp instead.
[deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
File "./src/IEEE754/PrimFloat.v", line 389, characters 47-57:
Warning: Notation ldexp_spec is deprecated since 8.15.0.
Use Z_ldexp_spec instead. [deprecated-syntactic-definition,deprecated]
Finished src/IEEE754/PrimFloat.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/IEEE754/Binary.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/IEEE754/Binary.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/IEEE754/Bits.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/IEEE754/Bits.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Calc/Plus.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Calc/Plus.vo
Building src/Pff/Pff2FlocqAux.vo
/usr/bin/coqdep -R src Flocq src/Pff/Pff2FlocqAux.v | ./remake -r src/Pff/Pff2FlocqAux.vo
Building src/Pff/Pff2Flocq.vo
/usr/bin/coqdep -R src Flocq src/Pff/Pff2Flocq.v | ./remake -r src/Pff/Pff2Flocq.vo
File "./src/Pff/Pff.v", line 16078, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16078, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16078, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16078, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16134, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16134, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16134, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16134, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16161, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16161, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16161, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 16161, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17313, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17313, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17313, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17313, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17436, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17464, characters 14-18:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17464, characters 14-18:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17466, characters 12-16:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17466, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17466, characters 12-16:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17466, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17467, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17468, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17468, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17469, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17469, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17469, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17470, characters 34-45:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17470, characters 47-51:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17470, characters 34-45:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17470, characters 47-51:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17471, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17471, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17471, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17472, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17472, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17478, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17478, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 9-13:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 37-48:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17480, characters 50-54:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17481, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17481, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17482, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17482, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17482, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17483, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17483, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17483, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17483, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17484, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17484, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17484, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17484, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17486, characters 19-22:
Warning: Notation odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17486, characters 19-22:
Warning: Notation odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17487, characters 17-33:
Warning: Notation not_even_and_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_Odd_False (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17487, characters 17-33:
Warning: Notation not_even_and_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_Odd_False (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 6-12:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 20-25:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 33-39:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 47-52:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 60-66:
Warning: Notation even_O is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_O instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 6-12:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 20-25:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 33-39:
Warning: Notation even_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 47-52:
Warning: Notation odd_S is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Odd_alt_S instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17489, characters 60-66:
Warning: Notation even_O is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt_O instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17490, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17490, characters 0-43:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17495, characters 8-12:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17495, characters 8-12:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17496, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17496, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17497, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17497, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17497, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17497, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17498, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17498, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17499, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17499, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17499, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17499, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17500, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17500, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17500, characters 31-42:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17500, characters 44-48:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17502, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17502, characters 0-55:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17503, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17503, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17503, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17510, characters 15-22:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17510, characters 15-22:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17511, characters 15-19:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17511, characters 15-19:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17512, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17512, characters 6-17:
Warning: Notation even_or_odd is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_or_Odd (together with Nat.Even_alt_Even and Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17513, characters 25-36:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17513, characters 38-42:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17513, characters 25-36:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17513, characters 38-42:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17514, characters 0-57:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17514, characters 0-57:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17515, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17515, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17515, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17515, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17516, characters 28-39:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17516, characters 41-45:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17516, characters 28-39:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17516, characters 41-45:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17518, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17518, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17519, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17519, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17519, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17519, characters 11-21:
Warning: Notation odd_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Odd_double (together with Nat.Odd_alt_Odd) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17643, characters 37-41:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17688, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17688, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17688, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17688, characters 12-18:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17734, characters 35-42:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17734, characters 35-42:
Warning: Notation lt_div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.lt_div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17735, characters 16-20:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17735, characters 16-20:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17736, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17736, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17736, characters 24-35:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17736, characters 37-41:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17737, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17737, characters 0-58:
Warning: Notation double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.double instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17738, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17738, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17738, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17738, characters 11-22:
Warning: Notation even_double is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.Even_double (together with Nat.Even_alt_Even) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17753, characters 33-37:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17787, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17814, characters 34-38:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17882, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17882, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17883, characters 40-44:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17884, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17883, characters 40-44:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17884, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17913, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17913, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17914, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17915, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17914, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 17915, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18040, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18067, characters 34-38:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18134, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18134, characters 39-43:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18135, characters 40-44:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18136, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18135, characters 40-44:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18136, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18165, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18165, characters 73-77:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18166, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18167, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18166, characters 52-56:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18167, characters 54-58:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18293, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18320, characters 33-37:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18349, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18509, characters 18-22:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18645, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18645, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18645, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18645, characters 11-17:
Warning: Notation S_pred is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_succ_pred (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18758, characters 18-22:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18892, characters 11-15:
Warning: Notation div2 is deprecated since 8.16.
The Arith.Div2 file is obsolete. Use Nat.div2 instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff.v", line 18919, characters 32-36:
Warning: Notation even is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even or Nat.Even_alt instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Pff/Pff.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Pff/Pff2FlocqAux.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
Finished src/Pff/Pff2FlocqAux.vo
/usr/bin/coqc  -R src Flocq -native-compiler yes src/Pff/Pff2Flocq.v
While loading initial state:
Warning: The native-compiler option is deprecated. To compile native files
ahead of time, use the coqnative binary instead.
[deprecated-native-compiler-option,deprecated]
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 902, characters 34-42:
Warning: Notation div_Zdiv is deprecated since 8.14.
Use Nat2Z.inj_div instead. [deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 943, characters 6-16:
Warning: Notation even_equiv is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_alt_Even instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Pff/Pff2Flocq.v", line 943, characters 6-16:
Warning: Notation even_equiv is deprecated since 8.16.
The Arith.Even file is obsolete. Use Nat.Even_alt_Even instead.
[deprecated-syntactic-definition,deprecated]
Finished src/Pff/Pff2Flocq.vo
Building all
Finished all
Building html/index.html
rm -rf html
mkdir -p html
/usr/bin/coqdoc -toc -interpolate -utf8 -html -g -R src Flocq -d html \
  --coqlib_url http://coq.inria.fr/distrib/current/stdlib \
  src/Version.v src/Core/Raux.v src/Core/Zaux.v src/Core/Defs.v src/Core/Digits.v src/Core/Float_prop.v src/Core/FIX.v src/Core/FLT.v src/Core/FLX.v src/Core/FTZ.v src/Core/Generic_fmt.v src/Core/Round_pred.v src/Core/Round_NE.v src/Core/Ulp.v src/Core/Core.v src/Calc/Bracket.v src/Calc/Div.v src/Calc/Operations.v src/Calc/Plus.v src/Calc/Round.v src/Calc/Sqrt.v src/Prop/Div_sqrt_error.v src/Prop/Mult_error.v src/Prop/Plus_error.v src/Prop/Relative.v src/Prop/Sterbenz.v src/Prop/Round_odd.v src/Prop/Double_rounding.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Binary.v src/IEEE754/Bits.v src/IEEE754/Int63Compat.v src/IEEE754/Int63Copy.v src/IEEE754/PrimFloat.v src/Pff/Pff.v src/Pff/Pff2FlocqAux.v src/Pff/Pff2Flocq.v
for f in html/*.html; do
  sed -e 's;<a href="index.html">Index</a>;Go back to the <a href="../index.html">Main page</a> or <a href="index.html">Index</a>.;' -i $f
done
Finished html/index.html
Building doc
Finished doc
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.yOHfdb
+ umask 022
+ cd /builddir/build/BUILD
+ '[' /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x '!=' / ']'
+ rm -rf /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x
++ dirname /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x
+ mkdir -p /builddir/build/BUILDROOT
+ mkdir /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x
+ CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection'
+ export CFLAGS
+ CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection'
+ export CXXFLAGS
+ FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules'
+ export FFLAGS
+ FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64 -march=z13 -mtune=z14 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib64/gfortran/modules'
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed  -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 '
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5
+ sed -i s,/usr/lib64,/builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/lib64, Remakefile
+ remake install
Building install
Finished install
+ cp -p src/Version.v /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/lib64/ocaml/coq/user-contrib/Flocq
+ cp -p src/Calc/Bracket.v src/Calc/Div.v src/Calc/Operations.v src/Calc/Plus.v src/Calc/Round.v src/Calc/Sqrt.v /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/lib64/ocaml/coq/user-contrib/Flocq/Calc
+ cp -p src/Core/Core.v src/Core/Defs.v src/Core/Digits.v src/Core/FIX.v src/Core/FLT.v src/Core/FLX.v src/Core/FTZ.v src/Core/Float_prop.v src/Core/Generic_fmt.v src/Core/Raux.v src/Core/Round_NE.v src/Core/Round_pred.v src/Core/Ulp.v src/Core/Zaux.v /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/lib64/ocaml/coq/user-contrib/Flocq/Core
+ cp -p src/IEEE754/Binary.v src/IEEE754/BinarySingleNaN.v src/IEEE754/Bits.v src/IEEE754/Int63Compat.v src/IEEE754/Int63Copy.v src/IEEE754/PrimFloat.v /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/lib64/ocaml/coq/user-contrib/Flocq/IEEE754
+ cp -p src/Pff/Pff.v src/Pff/Pff2Flocq.v src/Pff/Pff2FlocqAux.v /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/lib64/ocaml/coq/user-contrib/Flocq/Pff
+ cp -p src/Prop/Div_sqrt_error.v src/Prop/Double_rounding.v src/Prop/Mult_error.v src/Prop/Plus_error.v src/Prop/Relative.v src/Prop/Round_odd.v src/Prop/Sterbenz.v /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/lib64/ocaml/coq/user-contrib/Flocq/Prop
+ /usr/lib/rpm/check-buildroot
+ /usr/lib/rpm/redhat/brp-ldconfig
+ /usr/lib/rpm/brp-compress
+ /usr/lib/rpm/brp-strip /usr/bin/strip
+ /usr/lib/rpm/brp-strip-comment-note /usr/bin/strip /usr/bin/objdump
+ /usr/lib/rpm/redhat/brp-strip-lto /usr/bin/strip
+ /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip
+ /usr/lib/rpm/check-rpaths
+ /usr/lib/rpm/redhat/brp-mangle-shebangs
+ /usr/lib/rpm/brp-remove-la-files
+ /usr/lib/rpm/redhat/brp-python-bytecompile '' 1 0
+ /usr/lib/rpm/redhat/brp-python-hardlink
Processing files: flocq-4.1.0-2.fc38.s390x
Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.6NShhs
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5
+ DOCDIR=/builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/doc/flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export DOCDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/doc/flocq
+ cp -pr AUTHORS /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/doc/flocq
+ cp -pr NEWS.md /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/doc/flocq
+ cp -pr README.md /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/doc/flocq
+ cp -pr html /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/doc/flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.q37kqM
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5
+ LICENSEDIR=/builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/licenses/flocq
+ export LC_ALL=C
+ LC_ALL=C
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/licenses/flocq
+ cp -pr COPYING /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x/usr/share/licenses/flocq
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: flocq = 4.1.0-2.fc38 flocq(s390-64) = 4.1.0-2.fc38 ocaml(NFlocq_Calc_Bracket) = e0214f692ecd93d4c63ec81c9a68b962 ocaml(NFlocq_Calc_Div) = 7c60c3952e418096a31e27187b4dd54a ocaml(NFlocq_Calc_Operations) = 287d8ef36befd07a6aec3ba1b7c54b74 ocaml(NFlocq_Calc_Plus) = cd414e5fd77814d467c164f895edcb8c ocaml(NFlocq_Calc_Round) = 7c2bcdd8433b018527e07f973e03b2e3 ocaml(NFlocq_Calc_Sqrt) = dc80634ccb9f17f09e96b65b3d8ce0e6 ocaml(NFlocq_Core_Core) = 2fa7028371ef1690fbafb453d1753f36 ocaml(NFlocq_Core_Defs) = 08cd9b47bf7c432525e394f63175cafe ocaml(NFlocq_Core_Digits) = 3e3ce226aa583a7f62c6933c79a9587d ocaml(NFlocq_Core_FIX) = 67d75cf34e0a21bb4933d4ede0c59ebd ocaml(NFlocq_Core_FLT) = 8cdb39a38fe4b22eb6dfd1f6cc35ec2e ocaml(NFlocq_Core_FLX) = 9c1a23b9ba23e210b16128375943f9d5 ocaml(NFlocq_Core_FTZ) = 490f0c26edc460abe98e65100c33976e ocaml(NFlocq_Core_Float_prop) = 4b942fe265780af5750877ceb5d0a064 ocaml(NFlocq_Core_Generic_fmt) = 2410b3af617d927dd58d0b601b84c8bc ocaml(NFlocq_Core_Raux) = 34b3cbbefcc8082bfc2aa9bd75cb8316 ocaml(NFlocq_Core_Round_NE) = 397a14ff67db49a4decec417bef24e48 ocaml(NFlocq_Core_Round_pred) = c8db8a7cde956a4740a4a3a9a6acdcc9 ocaml(NFlocq_Core_Ulp) = ca08cb2d771a7819e3e0ca2fc95d54a1 ocaml(NFlocq_Core_Zaux) = 1331b523bdf9decaac86604d1dd39bbf ocaml(NFlocq_IEEE754_Binary) = bfe19cb133ebdf813649eadc9f7fa033 ocaml(NFlocq_IEEE754_BinarySingleNaN) = 46899ffb3587d90f885924e83c397f1b ocaml(NFlocq_IEEE754_Bits) = c18fb6385b8707fcac2e683795cf0082 ocaml(NFlocq_IEEE754_Int63Compat) = 3fedae605da4fecff3872eab98cb4f52 ocaml(NFlocq_IEEE754_Int63Copy) = 18ea296eb7d1692c25ab63c559a9e8a1 ocaml(NFlocq_IEEE754_PrimFloat) = fb2107011ebefcb731bf0ac8e5319ed8 ocaml(NFlocq_Pff_Pff) = e48189852892135fc83995c58946b6ab ocaml(NFlocq_Pff_Pff2Flocq) = ee7c1ac7d1d14a57619f17e45b77fbce ocaml(NFlocq_Pff_Pff2FlocqAux) = 9cace8df7df14405a2559db5b9301c3c ocaml(NFlocq_Prop_Div_sqrt_error) = 51c3c0a08720566b713df8887b365a13 ocaml(NFlocq_Prop_Double_rounding) = d498d71cbe0785a733ad17d130370f51 ocaml(NFlocq_Prop_Mult_error) = 6985758b26a828bf1c324d6b00fc7d69 ocaml(NFlocq_Prop_Plus_error) = 95fc4f7524d1dad2f13e35fd643c8568 ocaml(NFlocq_Prop_Relative) = 2b65cb4f202eb396ab08c703a10ea0c7 ocaml(NFlocq_Prop_Round_odd) = b59d9b3e3a8b8bd97b5a3a59dfb57a82 ocaml(NFlocq_Prop_Sterbenz) = 1a41570c6facab63d8799a06b647205b ocaml(NFlocq_Version) = dc1208bb5730ae7e4a2d6702d32cafc7 ocamlx(NFlocq_Calc_Bracket) = 82fd57fcd8dbe53929c8b442fc02076d ocamlx(NFlocq_Calc_Div) = 3f4d9a06599bb8c363de709173de11f1 ocamlx(NFlocq_Calc_Operations) = 9bcb0766ad7dbe8f6b9bec46d55c495b ocamlx(NFlocq_Calc_Plus) = 528304572035a8199bb7e010c736c4b5 ocamlx(NFlocq_Calc_Round) = 1e894b4ca8ff84e111b18c7c55bc2463 ocamlx(NFlocq_Calc_Sqrt) = 686477128b67289af20062ec501ac6b5 ocamlx(NFlocq_Core_Core) = d658f42381953d2c056571e767a06e49 ocamlx(NFlocq_Core_Defs) = d267aaa66dee1df5ed3fd3f0f19d6280 ocamlx(NFlocq_Core_Digits) = b0fa31117f100961bcc45d99aed81dce ocamlx(NFlocq_Core_FIX) = ab5e04c987d6e7f02380b1412ab173e0 ocamlx(NFlocq_Core_FLT) = 41dccf27c07e7191e7778d3e7e404511 ocamlx(NFlocq_Core_FLX) = a743a2a336654661abc14d4511cd781f ocamlx(NFlocq_Core_FTZ) = 7e92dc58854b7cc0ea7909e016c52d3a ocamlx(NFlocq_Core_Float_prop) = a65c20aa223a5a384d4d901c0f2d6e5c ocamlx(NFlocq_Core_Generic_fmt) = b343fea3302b6db51370de1ef4aa84c9 ocamlx(NFlocq_Core_Raux) = 81caaec2159d48d20c84ea046e2accc9 ocamlx(NFlocq_Core_Round_NE) = 49044a7a4324ede7469078aa5cc53724 ocamlx(NFlocq_Core_Round_pred) = da5024e18637a84a3322a70bd649f903 ocamlx(NFlocq_Core_Ulp) = a0e20ebabb635d2a72230bb2817b272a ocamlx(NFlocq_Core_Zaux) = 05fdc60c932a66243d8e6f7551011f8b ocamlx(NFlocq_IEEE754_Binary) = e0a122403194c7500b8bd5a00e785018 ocamlx(NFlocq_IEEE754_BinarySingleNaN) = f474171d39850ca15909537de7c9292a ocamlx(NFlocq_IEEE754_Bits) = 860230c1a0f24f15a32705a6e396f30a ocamlx(NFlocq_IEEE754_Int63Compat) = bde0a846521c3cb4f519fa383559ab49 ocamlx(NFlocq_IEEE754_Int63Copy) = 78f8c2a62f4fb58e22aeda8c19388eb6 ocamlx(NFlocq_IEEE754_PrimFloat) = ce30eaf89bf4cea1c1aa83b6d6554ef8 ocamlx(NFlocq_Pff_Pff) = 87d72918d6a5ecb6914e0c51b434dcb3 ocamlx(NFlocq_Pff_Pff2Flocq) = c8980122fe1b07f6fa1a04d4895a445c ocamlx(NFlocq_Pff_Pff2FlocqAux) = 1bc7ff59daf843c84ab9acd522c9c604 ocamlx(NFlocq_Prop_Div_sqrt_error) = cde0ff580280ac6b63d13b1c3f6cad15 ocamlx(NFlocq_Prop_Double_rounding) = 7a6bcb39bcd62c2303a3cf6dbf1efb00 ocamlx(NFlocq_Prop_Mult_error) = 0885bde4f02a7b341ef5aca2afa6d72e ocamlx(NFlocq_Prop_Plus_error) = 11ea05686dce8f74d7a101630ced3969 ocamlx(NFlocq_Prop_Relative) = 1418ea6985a6f60cab3fda1594848ce3 ocamlx(NFlocq_Prop_Round_odd) = 8706865dabf34362a480ae27a426a989 ocamlx(NFlocq_Prop_Sterbenz) = f92f396e824ea6e9f43929cac49f8298 ocamlx(NFlocq_Version) = a4fa2dcfa23afc22392694daa8691955
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Requires: ocaml(AcyclicGraph) = 00edc3e526b6239e9ad4c9319eaaabd5 ocaml(CArray) = 3bf67d1381824155797389de8a32d728 ocaml(CAst) = b49a9e05558d074ce2420f1481d80d8a ocaml(CDebug) = a0c286baa9a2b79d6bec187ce25083a3 ocaml(CEphemeron) = 7a5613ac8c99a7839b27f0eb26c409cc ocaml(CList) = a742212da585b925999bb1e9c57f8886 ocaml(CMap) = cbcf10800400dde7f75cbc0cc6a0a739 ocaml(CPrimitives) = 98ddda2b8661651d0ac1c4d2f3adc78a ocaml(CSet) = 10548a97a94e3c63dea0f824f53da608 ocaml(CSig) = 93d511bb9f97d6117a9dba3706ab0743 ocaml(CString) = f53fe8692b6d16ecf125c5433c67ee1d ocaml(CUnix) = 59f179ae315fc18388551aa9972e0dfc ocaml(CamlinternalFormatBasics) = 8f8f634558798ee408df3c50a5539b15 ocaml(CamlinternalLazy) = 5365fec4a58da3e2d8fa2186f77d9be4 ocaml(Constr) = 9ca352bce78df900bce25f5e83b3e3ec ocaml(Context) = 233f361cbf25095b743d2afa636ee001 ocaml(Conv_oracle) = a9dd31ebef4b0f31606274cf6690f783 ocaml(Cooking) = c511194cd3d1c75d0ec51fe57d5c4b93 ocaml(Declarations) = af077788df86ae3c100cb12d0e433100 ocaml(Environ) = 81958cbbb97b08eb74f21205ecbe734b ocaml(Esubst) = 746f3c41caf469b8602bbc0673a9de61 ocaml(Evar) = 156cdf64bb05c4ab0c4051f998dfab52 ocaml(Exninfo) = 766d613c58c5e25783f49ff1e5b36922 ocaml(Float64) = 712fa5d21be885f62f4afb0c1b2e620e ocaml(Hashcons) = 04171b8e413a80692dcbea1031ff4542 ocaml(Hashset) = b5af2da2ba0f0aa4ffcd46fea97b6074 ocaml(Int) = c638a3a3a3350b9a3cd3aecfc1548b44 ocaml(Loc) = de5fd01aaa49ae97f2332d9b30807adc ocaml(Mod_subst) = b56a185b9f7bb6f0f0f519c06bf981db ocaml(NCoq_Arith_Factorial) = edee5881ef17d727e3ee1030d7a1e5d2 ocaml(NCoq_Arith_PeanoNat) = 3922c4f429b4350bba2dd2dab23b5b5a ocaml(NCoq_Bool_Bool) = 0804aef187ec6ef5a4c6bc88c0a4973b ocaml(NCoq_Bool_Sumbool) = d2613c6f687e37311723c347656b1afa ocaml(NCoq_Classes_Morphisms) = 6b266a73e315469f08ebc542bf8746e8 ocaml(NCoq_Classes_Morphisms_Prop) = c52138961674f9ee5fab86bc21830c4a ocaml(NCoq_Classes_RelationClasses) = 03470792223f41943cca775a8537bcad ocaml(NCoq_Floats_FloatAxioms) = 8203fcfc25e03e0df4b03b958f6cd22f ocaml(NCoq_Floats_FloatClass) = 9a5e5f319332f1aab08117fc52822560 ocaml(NCoq_Floats_FloatOps) = 4bf94eb06294927847fbdd30435cf03d ocaml(NCoq_Floats_PrimFloat) = a74da887993f30bc7a27941ede275b23 ocaml(NCoq_Floats_SpecFloat) = 18edf3f67606ec5d149da16e9c2c1dcc ocaml(NCoq_Init_Datatypes) = 7dff06490587ae72d8c480e28d0792c8 ocaml(NCoq_Init_Decimal) = 0091886e0df87b48c1b71a630733d322 ocaml(NCoq_Init_Hexadecimal) = 48f69a780f3ab731bfd5fd9892b611dc ocaml(NCoq_Init_Logic) = 8d49d9267163e6178eb2130b0afa5363 ocaml(NCoq_Init_Nat) = ba503b0fd72b1b323ac75b26585630aa ocaml(NCoq_Init_Number) = cd525699ffce1c8a6f907027bb87d10f ocaml(NCoq_Init_Peano) = 67f231ba5cf8725357b5682f1d4ed41b ocaml(NCoq_Init_Specif) = 6ee28c2862fc7fd46a5168a9f874140a ocaml(NCoq_Init_Wf) = 5bca515f37535f096c090facf9f2ee7b ocaml(NCoq_Lists_List) = f0f59ccc11cabe932e06f5bc97cf054c ocaml(NCoq_NArith_BinNat) = d014d8a7617cce07faeac7a778ef66c6 ocaml(NCoq_Numbers_BinNums) = f68e6acf6ffb202993bf722adf5f5260 ocaml(NCoq_Numbers_Cyclic_Abstract_CarryType) = 2069f40d947cb704ed777599406be7e5 ocaml(NCoq_Numbers_Cyclic_Int63_PrimInt63) = cf3af728d29cb993618f0a2c51ef0c6d ocaml(NCoq_Numbers_Cyclic_Int63_Uint63) = 682d2083bc134da2d0ac554274b220af ocaml(NCoq_PArith_BinPos) = 567a8354cd285d3669d47d582c454eca ocaml(NCoq_Program_Basics) = 819299f98ae3fdc97e4a9a2c9609ffae ocaml(NCoq_QArith_QArith_base) = e89b31eaa6e00a18da0fbd5d08938402 ocaml(NCoq_QArith_Qabs) = 4a3dc52bf2666912d7d251574a7b8367 ocaml(NCoq_QArith_Qreduction) = 648dbc98464b2098597c04a9e931ceff ocaml(NCoq_Reals_Alembert) = b40922aa694cb517278c619534d861c9 ocaml(NCoq_Reals_Cauchy_ConstructiveCauchyReals) = 3bc9cae9c5f4257f9935585d0566e119 ocaml(NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult) = d0cfbe899abd4907c1c20c02ebd67b98 ocaml(NCoq_Reals_Cauchy_QExtra) = 416b35c7119a55b95616d5ab474212b9 ocaml(NCoq_Reals_RIneq) = e17d1e4cd82578c36d0c8b465e5d0fcc ocaml(NCoq_Reals_R_sqrt) = 0ef21d135ce5620dcdffd8943721e056 ocaml(NCoq_Reals_Raxioms) = 8717e5ba29c58e18675aa9d4441687b9 ocaml(NCoq_Reals_Rbasic_fun) = d7937acd1fa489b5786486500a1c33c7 ocaml(NCoq_Reals_Rdefinitions) = f36e6fdcfa9a0e339578e20a9f5db7d3 ocaml(NCoq_Reals_Rfunctions) = bee964dae118e2f605da619804d4e408 ocaml(NCoq_Reals_Rpow_def) = 08d14df826ae8289b86b0107fb9c36d6 ocaml(NCoq_Reals_Rpower) = 8767217ef0eaef18c23c7865242cf7ba ocaml(NCoq_Reals_Rsqrt_def) = f42bf05072ae26906298ececd08c0f21 ocaml(NCoq_Reals_Rtrigo_def) = c17a6892fc43af795a51e11b6790caaa ocaml(NCoq_Reals_Rtrigo_fun) = c1ae23fc6d3a0c86eda15d3db1b1fd77 ocaml(NCoq_Relations_Relation_Definitions) = 50d48e86dd918045ba6710f690346c4e ocaml(NCoq_Structures_OrdersTac) = e653cee5a401486b918c1d13e4ee646c ocaml(NCoq_ZArith_BinInt) = 75a2ff407fbbc12c0021cf14b6cb0f4a ocaml(NCoq_ZArith_BinIntDef) = 4334d3b5d9b98827dd666f7d25d45dad ocaml(NCoq_ZArith_ZArith_dec) = 127ab251d986c70c3d6131d06396afd8 ocaml(NCoq_ZArith_Zbool) = 3c79cf9f91dd9622e786c53f032964e0 ocaml(NCoq_ZArith_Zeven) = 62d38b4a4e33dc0f927bb81a7f738a3e ocaml(NCoq_ZArith_Znat) = e6a528fc72a76ccc4ceb24d48ae0dfd1 ocaml(NCoq_ZArith_Zorder) = b5f838424961c1897d441dd879a192ad ocaml(NCoq_ZArith_Zpower) = 2404fff785da3403be59e3b5070915a7 ocaml(NCoq_setoid_ring_Ring_theory) = 6b85b253533d9c96b7b96cbbf6e15a26 ocaml(NFlocq_Calc_Bracket) = e0214f692ecd93d4c63ec81c9a68b962 ocaml(NFlocq_Calc_Operations) = 287d8ef36befd07a6aec3ba1b7c54b74 ocaml(NFlocq_Calc_Round) = 7c2bcdd8433b018527e07f973e03b2e3 ocaml(NFlocq_Core_Defs) = 08cd9b47bf7c432525e394f63175cafe ocaml(NFlocq_Core_Digits) = 3e3ce226aa583a7f62c6933c79a9587d ocaml(NFlocq_Core_FIX) = 67d75cf34e0a21bb4933d4ede0c59ebd ocaml(NFlocq_Core_FLT) = 8cdb39a38fe4b22eb6dfd1f6cc35ec2e ocaml(NFlocq_Core_Generic_fmt) = 2410b3af617d927dd58d0b601b84c8bc ocaml(NFlocq_Core_Raux) = 34b3cbbefcc8082bfc2aa9bd75cb8316 ocaml(NFlocq_Core_Ulp) = ca08cb2d771a7819e3e0ca2fc95d54a1 ocaml(NFlocq_Core_Zaux) = 1331b523bdf9decaac86604d1dd39bbf ocaml(NFlocq_IEEE754_Binary) = bfe19cb133ebdf813649eadc9f7fa033 ocaml(NFlocq_IEEE754_BinarySingleNaN) = 46899ffb3587d90f885924e83c397f1b ocaml(NFlocq_Pff_Pff) = e48189852892135fc83995c58946b6ab ocaml(Names) = 0b6c349e44c595f40356f60ca49fa766 ocaml(Nativecode) = 02dbeca2f7bfac8ee80f221d7d1bcb8a ocaml(Nativeconv) = 60d8b9f9f4561c30226973b77f29c919 ocaml(Nativelambda) = 219578857e7b319faa4d145a4fa5ff68 ocaml(Nativelib) = 7b23ee7251439aa612f59354c020ea67 ocaml(Nativevalues) = 151356e5f71c48ba131e257d7b5d6b0e ocaml(Opaqueproof) = b1745fe14cd37c212d34eea094f1b8df ocaml(Parray) = 3587b91abccbee918d16a0ecc7071866 ocaml(Pp) = b42c7d685f7cf8e56cb9e5cb72b082aa ocaml(Predicate) = e10f527c1e68b4fcf4187c345bdd22e5 ocaml(Range) = 346d147227354e938de6b932d04d6b3d ocaml(Reduction) = 3523f631320a31383fd961d753a8e437 ocaml(Retroknowledge) = 921f47b24ba103d9c6a00670a3a8a6c8 ocaml(Rtree) = 3aeff8b2ebba7f5453fc613375ce0644 ocaml(Sorts) = e73c70ce289f5c49f0cf7f5a0ceeefc2 ocaml(Stdlib) = 6d7bf11af14ea68354925f3a37387930 ocaml(Stdlib__Array) = 622d88fad859d0d0f019e691fc4fa865 ocaml(Stdlib__Bigarray) = 994a14f10d5ae081663b52b790ee11d3 ocaml(Stdlib__Buffer) = 4b09c9a6d0622bbf5a3829234b481822 ocaml(Stdlib__Complex) = 4555217c759e89d65daa8f682eb09b35 ocaml(Stdlib__Either) = 26845df28d19584687a38a1ab814c3f9 ocaml(Stdlib__Format) = b6edb97b685819e873481fe05723c8bc ocaml(Stdlib__Int32) = a71ea5238030770647165f659f80b1ab ocaml(Stdlib__Int64) = 0fa5587c47baf16a06837c7dedfc2518 ocaml(Stdlib__Lazy) = 01430d340c028322c7247031a874e355 ocaml(Stdlib__List) = ee222542f6f8195441543b8b399b64b9 ocaml(Stdlib__Map) = 978f82916b5a172c11d2b72719d85680 ocaml(Stdlib__Obj) = 25794d29f7f4018768ea900e331a2bf3 ocaml(Stdlib__Seq) = b63511032211eae4b567ba313cd72962 ocaml(Stdlib__Set) = 871d2ee2167ac9e7977fa13994cf4658 ocaml(Stdlib__Stream) = 510a78f010f6c530a911189d7538d002 ocaml(Stdlib__String) = 097838f294457ecbb61ccbcf86cc6972 ocaml(Stdlib__Uchar) = c0dde02a556a6d79e363ad365d165d57 ocaml(Term) = c1500a859572f47c5adeb740fbcebf6b ocaml(TransparentState) = 1dab58426370af71f458b92a6fb5ef06 ocaml(UGraph) = bd28bddd5c33ca5c1a5f9f43f907e5da ocaml(Uint63) = 5150bcb618feddc1f891db28ba2fa04b ocaml(Univ) = 6feb5ec642e4daf30a0944e888214cea ocaml(Unix) = 84bb8ec8ae50f70acba86f5b72088b1c ocaml(Util) = 46a1f0249bfbf29202e10de25200d4ea ocaml(Vmbytecodes) = 88733f1084158f9273bb318495213675 ocaml(Vmemitcodes) = 2ee3a68ca9992bc9e1f6aeb9e6e33af6 ocaml(Vmvalues) = 6cfd8f0d13168b127ebed3d4375b15c3 ocamlx(CamlinternalLazy) = 7498a48b2fe233db683be47d48c215fc ocamlx(NCoq_Bool_Bool) = 3f077edca92ed17f44c66137c4136c04 ocamlx(NCoq_Floats_FloatAxioms) = d197e518b29a0b9adc4a3ec393a06902 ocamlx(NCoq_Floats_FloatOps) = 955c1fd2218169d08e022e293c75ab08 ocamlx(NCoq_Floats_SpecFloat) = c356ad7392a9629e0a65ec307a06bfa3 ocamlx(NCoq_Init_Datatypes) = cdbab4b0bd137a1bc00d54561f3dd061 ocamlx(NCoq_Init_Logic) = 41d65a6a2b1c55d6e2f10cf6ded4b229 ocamlx(NCoq_Init_Nat) = 64321e52710eeaa352d709d8ccafe6cf ocamlx(NCoq_Init_Specif) = deb5ee0a23525d72a763da2cf5baa68d ocamlx(NCoq_Lists_List) = 8907851d368bbc622072348a2536b0a3 ocamlx(NCoq_NArith_BinNat) = 19dc97790aa8fd60b0b8835c17ab2206 ocamlx(NCoq_Numbers_BinNums) = e0612228d82543c6ffaaa7a7352608e9 ocamlx(NCoq_PArith_BinPos) = 1e8b3ca260e0a0ff81f3991f27f1be38 ocamlx(NCoq_Reals_RIneq) = 37d05c1cbbb0b1be712c17e4be627ac1 ocamlx(NCoq_Reals_R_sqrt) = 27b338f7a9c7ab544cf1067dbd948ae9 ocamlx(NCoq_Reals_Rbasic_fun) = 2c165e553032f50d013dc3e0ad2b2069 ocamlx(NCoq_Reals_Rdefinitions) = 8a9cac064a58a982fe19448f6fbaa88d ocamlx(NCoq_Reals_Rfunctions) = 619dbcc0d97ba223da5000be188b512b ocamlx(NCoq_Reals_Rpower) = a6988a1bdaab201398cfba5ef90521c2 ocamlx(NCoq_ZArith_BinInt) = 72c720a0aa3efbe0e6c6319c8bf70f35 ocamlx(NCoq_ZArith_BinIntDef) = c41b7ecc88fb8f2ffc74fd632188d192 ocamlx(NCoq_ZArith_ZArith_dec) = e7a44ad0178530c860fa5a0e5d0b1179 ocamlx(NCoq_ZArith_Zbool) = 385a4314bd8a1898f5ec08d609499805 ocamlx(NCoq_ZArith_Zorder) = 8601a05a7fe9d375161317c881a7886d ocamlx(NCoq_ZArith_Zpower) = 277dd7090eabd4d926b59df95dc9bfc3 ocamlx(NFlocq_Calc_Bracket) = 82fd57fcd8dbe53929c8b442fc02076d ocamlx(NFlocq_Calc_Operations) = 9bcb0766ad7dbe8f6b9bec46d55c495b ocamlx(NFlocq_Calc_Round) = 1e894b4ca8ff84e111b18c7c55bc2463 ocamlx(NFlocq_Core_Defs) = d267aaa66dee1df5ed3fd3f0f19d6280 ocamlx(NFlocq_Core_Digits) = b0fa31117f100961bcc45d99aed81dce ocamlx(NFlocq_Core_FIX) = ab5e04c987d6e7f02380b1412ab173e0 ocamlx(NFlocq_Core_FLT) = 41dccf27c07e7191e7778d3e7e404511 ocamlx(NFlocq_Core_Generic_fmt) = b343fea3302b6db51370de1ef4aa84c9 ocamlx(NFlocq_Core_Raux) = 81caaec2159d48d20c84ea046e2accc9 ocamlx(NFlocq_Core_Ulp) = a0e20ebabb635d2a72230bb2817b272a ocamlx(NFlocq_Core_Zaux) = 05fdc60c932a66243d8e6f7551011f8b ocamlx(NFlocq_IEEE754_Binary) = e0a122403194c7500b8bd5a00e785018 ocamlx(NFlocq_IEEE754_BinarySingleNaN) = f474171d39850ca15909537de7c9292a ocamlx(NFlocq_Pff_Pff) = 87d72918d6a5ecb6914e0c51b434dcb3 ocamlx(Nativecode) = 0798b9a570319ea4c985f1a8a57f0c97 ocamlx(Nativevalues) = 7774b44ec1e54680f312f408409ec824 rtld(GNU_HASH)
Processing files: flocq-source-4.1.0-2.fc38.s390x
Provides: flocq-source = 4.1.0-2.fc38 flocq-source(s390-64) = 4.1.0-2.fc38
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x
Wrote: /builddir/build/RPMS/flocq-source-4.1.0-2.fc38.s390x.rpm
Wrote: /builddir/build/RPMS/flocq-4.1.0-2.fc38.s390x.rpm
Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.saxHfZ
+ umask 022
+ cd /builddir/build/BUILD
+ cd flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5
+ /usr/bin/rm -rf /builddir/build/BUILDROOT/flocq-4.1.0-2.fc38.s390x
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(rmbuild): /bin/sh -e /var/tmp/rpm-tmp.r9Grnp
+ umask 022
+ cd /builddir/build/BUILD
+ rm -rf flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5 flocq-flocq-4.1.0-0188199cb28d89a73937d009d935b016e2d394b5.gemspec
+ RPM_EC=0
++ jobs -p
+ exit 0
Child return code was: 0